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.

Downloads

SASyLF is available from GitHub. It's easiest to use SASyLF in an IDE; we have support for VSCode and Eclipse.
The VSCode plugin is available by searching for SASyLF in the Extensions: Marketplace section of VSCode. You can also find it online.
To install the Eclipse plugin, download the latest jar file, move the jar file to the dropins/ directory within Eclipse, and restart Eclipse. Note: we've found that MacOS users may need to do this in a fresh copy of Eclipse.

Documentation

More detailed Installation instructions.
POPL 2023 tutorial on teaching with SASyLF: video, slides, zip of exercises and homework curricula, and setup instructions.
Syntax of declarations and theorems
Writing proofs in SASyLF

Papers

Jonathan Aldrich, Robert J. Simmons, and Key Shin. SASyLF: An Educational Proof Assistant for Language Theory. In Proceedings of Functional and Declarative Programming in Education, 2008.

News

Thanks to John Boyland for making major recent updates to SASyLF and its Eclipse IDE!
The SASyLF source code is available at GitHub.
An Eclipse plugin is available with each Github release.
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 and Todd Millstein) Fall 2008-Fall 2011. Student post-survey results from 2008 included (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: 4.0
- 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 describing the motivation for the tool and initial experience in the classroom. We 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.

Indonesian translation of this page courtesy of Jordan Silaen at ChameleonJohn.com. Hungarian translation of this page courtesy of Elana Pavlet.