Possible Advanced Undergraduate or Masters' Projects on SASyLF

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.

Testing

Currently SASyLF has about 90 test files to run against whenever a change is made to the engine (regression tests). One project would be to provide test cases that provide full coverage of every error message, or even full coverage of every line in the core.

Tool Support

SASyLF is currently supported by an Eclipse plugin. The following project outlines are on improving this support.

Refactoring

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

Incrementality

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.

Implementation

Automated theorem proving

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.

Compilation

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.

Extensions

The following and other extensions are discussed to some extent on the SourceForge SASyLF discussion forum. Here they are listed in approximate increasing complexity.
  1. Syntactic sugar, both for syntax and for judgments.
  2. Reduction proofs, so that (for example) from n1 > n2, SASyLF would permit an inductive call to use the second in place of the first.
  3. Modules
  4. Function Syntax
  5. Coinduction
  6. Explicit contexts.

Use

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: August 6, 2016