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 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. We have some preliminary experience teaching with
SASyLF in a graduate Analysis course at Carnegie Mellon University.
News
- We have developed a preliminary solution to the POPLmark challenge
Downloads
Papers