An in-progress port of LambdaPi to Standard ML
Standard ML
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
.gitignore
EVAL.sig
QUOTE.sig
README.md
SYN.sig
TYPING.sig
eval.fun
main.sml
quote.fun
syntax.sml
typing.fun

README.md

This is (so far) a port of Löh/McBride/Swierstra's Lambda-Pi to Standard ML. Mostly so that I can learn SML, and think about modular development.

Eventually, I'll probably use this as yet another place to fiddle with various notions of equality, including OTT and ETT.