This project is an interpretor for Pure Type Systems, a family a typed λ-calculi.
You can try it online on the github pages
opam install . -y --deps-onlydune build
This interpretor :
- check if the file is well typed (with the option
type_debug, it prints on stdout the typing judgments used, and with the option--get-proof, it prints the proof on a.texfile) - If the file is well typed, then it computes its normal form
Supported extension :
.stlcfor simply typed λ-calculus.ffor System F (simply-typed λ-calulus with polymorphism).fwfor System Fω (System F with type constructor).ccfor the Calculus of Constructions.ufor the System U (beware that it's an inconsistent system)
Type ./pts.exe -help to see the list of options.
TODO:
- adding axioms (e.g. for λ0)