Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 SASyLF: An Educational Proof Assistant for Language Theory
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. 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
Current SASyLF release (400k zip,
includes source)