Implementation of some type theories in ELPI, an embeddable λProlog interpreter, as part of a curricular internship with professor Claudio Sacerdoti Coen.
These theories can be used to prove some (basic) theorems using the interactive theorem prover found in itp.elpi. Given a type it gradually builds a typed λ-term through the use of tactics given as input by the user.
stlc contains term definitions, typing, conversion and tactics for the simply typed λ-calculus.
itt contains all of the above for a fragment Martin-Löf's Intuitionistic Type Theory (namely pi, sigma and nats).
Who could have guessed it! Go here.
- Create a file where you'll put what you want to prove,
- using
accumulateaddstlc/theoryoritt/theoryto accumulate the whole "theory", - accumulate the
itpand start the itp loop by- writing something like
of X TypeDeclwhereTypeDeclis what you want to prove and - running the actual loop using:
run_itp X InScriptwhereInScriptis a list of tactics that can be given as input.
- writing something like
As an example of how one such file could look see test_itt.elpi.