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
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
- Current SASyLF release available from SourceForge. The "zip" file includes the sources and the command-line executable. The "jar" file is the Eclipse plugin.
- Thanks to John
for making major recent updates to SASyLF and its Eclipse IDE!
- The SASyLF source code is available at Google Code.
- An Eclipse plugin
SASyLF IDE is now
available (link is to a jar).
- Subscribe to the sasylf-announce
Google Group to get announcements related to SASyLF releases and
events, and to the sasylf-users
group for questions and other discussions regarding SASyLF.
- SASyLF was used in two graduate type theory courses (taught by John Boyland
Millstein) Fall 2008-Fall 2011. Student post-survey results from
(Likert scale 1-5, 5 is strongly agree):
- Would like to use SASyLF in another PL course: 4.2
- Able to learn SASyLF quickly: 3.8
- SASyLF improved my ability to prove theorems, even on paper:
- SASyLF enabled me to accomplish tasks more quickly: 3.3
- Rob Simmons designed a super-cool Sassy Elf, with an uncanny
resemblance to the Twelf Elf.
- At ICFP '08,
presented a paper at the FDPE workshop
motivation for the tool and initial experience in the classroom.
also gave an informal presentation on the system's semantics at WMM,
and have a poster at the main conference.
- We have developed a preliminary solution
to the POPLmark challenge.
Thanks to our Sponsors!
This work was supported in part by NSF CAREER award CCF-0546550, DARPA
grant HR00110710019, the Department of Defense, and an NSF Graduate
Research Fellowship for Robert J. Simmons. Any
opinions, findings and conclusions or recomendations expressed in this
material are those of the author(s) and do not necessarily reflect the
views of the National Science Foundation (NSF), DARPA, or the
Department of Defense.