SASyLF is a proof assistant that uses a style as close as possible to paper proofs while being very explicit. It is used as a teaching tool for graduate type theory courses based on Pierce's Types and Programming Languages textbook. We are working to make SASyLF more powerful and to give it better tool support.

judgment eval : ⟨µ,s⟩ →g ⟨µ,s⟩ ⟨µ,s1⟩ →g ⟨µ',s1'⟩ ------------------------- E-Par1 ⟨µ,(s1‖s2)⟩ →g ⟨µ',(s1'‖s2)⟩ ... lemma lem4: forall iso: µ1 ~ µ2 forall eval: ⟨µ1,s⟩ → g ⟨µ1',s'⟩ exists µ2' ~ µ1' and ⟨µ2,s⟩ → g ⟨µ2',s'⟩. proof by ... end lemma

This page lists various projects that an advanced undergraduate student or a graduate student could do with me. The precise scope of the project would be worked out in advance. The project could be an independent study, a master's capstone or a master's thesis, depending on the scope.

Eclipse supports refactoring on Java programs; we'd like to add refactoring support for SASyLF proofs:

- Renaming: rules, theorems, derivations, pattern variables.
- Syntax refactoring: changing the syntax of terms or of a judgment. The ability to add or remove "children" is harder but very useful as well.
- Change signature of a rule or theorem: add or remove inputs or (for a theorem) outputs. This gets particular interesting with inductive proofs.
- Lemma extraction/inlining.

Currently the plugin re-checks the entire file whenever one requests a check. It would make sense to just re-check the parts that changed or are affected by a change.

SASyLF has a `... by solve` syntax but the theorem prover
never was very good and has not been updated to handle any changes
since the 1.0.2 release.
At the very least, it should handle calling rules and lemmas, but it
would be nice to have extensions to handle built-in proof steps such as
weakening, exchange and substitution. Other extensions include case
analysis of `or` constructs.

SASyLF uses constructive logic and should be runnable. This
project would make SASyLF proofs into an executable program with the
parser used to construct inputs for a 'main' theorem.
An `unproved` step represented a (fatal) exception or a
break-point. A "debugger" could be used to examine the state of the
system at such a point and perhaps construct a derivation on the fly
to permit continued execution.

Along with compilation, one could implement a dynamic search tool that interprets the rules as glorified horn clauses and can be run to search for a derivation meeting certain criteria.

- Syntactic sugar, both for syntax and for judgments.
- Reduction proofs, so that (for example) from
*n*_{1}>*n*_{2}, SASyLF would permit an inductive call to use the second in place of the first. - Modules
- Function Syntax
- Subnonterminals (e.g. "values"). This requires adding subtyping to LF (which has been done before).
- Coinduction
- Explicit contexts.

I'd be interested in someone mechanizing a proof for another group/professor using SASyLF. In particular, it would help find bugs and prioritize suggested enhancements. I'd be happy to be involved helping to use the tool and adding what features, fixing what bugs as possible.

Last Update: December 11, 2017