SASyLF: An Educational Proof Assistant
for Language Theory
Teaching and learning formal programming language theory is hard, in
part because it's easy to make mistakes and hard to find them.
Proof assistants can help check proofs, but their learning curve is too
steep to use in most classes, and is a barrier to researchers too.
SASyLF (pronounced "Sassy Elf") is an LF-based proof assistant
specialized
to checking theorems
about programming languages and logics. SASyLF has a simple
design philosophy: language and logic syntax, semantics, and
meta-theory should be written as closely as possible to the way it is
done on paper. SASyLF can express proofs typical of an
introductory graduate type theory course. SASyLF proofs are
generally very explicit, but its built-in support for variable binding
provides substitution properties for free and avoids awkward variable
encodings.
News
- SASyLF is being used in at least two graduate type theory courses
in Fall 2008!
- Rob Simmons designed a super-cool Sassy Elf, with an uncanny
resemblance to the Twelf Elf.
- At ICFP '08,
we will present a paper at the FDPE workshop
describing the
motivation for the tool and initial experience in the classroom.
We
will also give an informal presentation on the system's semantics at WMM,
and will have a poster at the main conference.
- We have developed a preliminary solution
to the POPLmark challenge.
Downloads
- Current SASyLF release, version 0.19
(480k zip,
includes sources)
Papers