Logic & Languages @ CMUQ
Sequoia
A web application for defining sequent calculus, building proof trees,
and proving meta-properties.
website | source
To do:
- Clean up unused libraries. Refactor code according to Software Engineering best practices.
- Modify grammar to support more complex languages (e.g. 15-316 systems).
- Export systems to a proof assistant (Coq, Isabelle, Lean, etc.)
SMLtoCoq
A software that translates SML code into Coq definitions, and SML
annotations into Coq theorems.
source
To do:
Silkie
A web application for 15-150 students to prove properties about SML
functions in Coq.
website | source
To do:
- Study whether the Coq code can be completely hidden.
- Test it with 15-150 students.
Py★
Formalization and implementation of Python's bytecode execution
machinery
source
To do:
- Extensive testing with cpython's test suite.
Djed
Formalization and implementation of the Djed stablecoin.
website | source
To do:
- Formalize oracles with multiple owners.
- Study aggregation mechanisms.
Random ideas
- Image recognition tool for transforming written proof trees into LaTeX.