[TYPES/announce] SASyLF educational proof assistant

[Jonathan Aldrich]

I'm pleased to announce the availability of the SASyLF educational proof 
assistant for the meta-theory of programming languages and logics. 
SASyLF ("Sassy Elf") has a simple design philosophy: language and logic 
syntax, semantics, and meta-theory are written as closely as possible to 
the way they are written on paper.  This design choice means the tool 
can be adopted with little or no in-class instruction and with a minimal 
learning curve.  Error messages are effectively localized and are 
presented in terms of student-understandable concepts.

SASyLF can express many proofs typical of an introductory graduate type 
theory course; for example, we have developed a preliminary solution to 
part 2A of the POPLMark challenge, i.e. type soundness for System F-sub 
(see the site below).  SASyLF proofs are generally very explicit, but 
its built-in support for variable binding (the "LF" in SASyLF) provides 
substitution properties for free and avoids awkward variable encodings.

Type theory researchers looking for a proof assistant with a gentle 
learning curve may also find SASyLF useful, with the caveat that proofs 
are likely to be somewhat more verbose than in existing theorem provers 
that focus on a research, rather than an educational, audience.

The current release (version 0.7) is relatively stable and implements 
most checks, including rule application, correct and completeness case 
analysis, and uses of lemmas and the induction hypothesis.  A few checks 
are still unimplemented, including those for substitution, weakening, 
exchange, and contraction--these features can be used but are not 
checked.  We hope to implement these checks in the very near future, but 
decided to announce the tool as we believe it is mature enough to be 
useful in Fall courses.  The open-source tool and more information is 
available at:


http://www.sasylf.org/


We will present initial educational experience with SASyLF in a FDPE '08 
workshop paper (available at the site above), and will describe the 
design of the tool in WMM '08.  Also look for our poster at ICFP.  If 
you're interested in using the tool in a course, but need some feature 
badly, please let me know, as I'd like to gather experience teaching 
with SASyLF.

Thanks,

Jonathan Aldrich


P.S. For those who know Ott, SASyLF's syntax for definitions is similar. 
  Unlike Ott, we go beyond definitions to express and check *proofs* in 
a friendly, paper-like notation.