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:
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.
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