A typechecker for intensional MLTT without elaboration.

Go to file

Rachel Lambda Samuelsson fcd2ec66e8 added let in to TODO		2022-07-21 04:19:47 +02:00
src	added Σ types	2022-07-21 04:18:50 +02:00
.gitignore	initial commit	2022-04-23 15:18:06 +02:00
README.md	added let in to TODO	2022-07-21 04:19:47 +02:00
makefile	initial commit	2022-04-23 15:18:06 +02:00
pi.ipkg	it works ! a lot has changed	2022-05-13 19:46:05 +02:00

README.md

pi

A dependently typed system

Implemented

A Basic dependent lambda calculus
- lambda abstractions
- variables
- pi types
- type of types
Unit type
Empty type
Natural numbers

TODO

Let … in …
Fun types
- Id
Parser
Implicit arguments
Universes
(indexed) inductive datatypes
Write down the rules (I’ll not get this far)

References

Some of the material I found helpful in groking dependent type checking:

Coquand, Thierry. “An Algorithm for Type-Checking Dependent Types.” Science of Computer Programming 26, no. 1–3 (May 1996): 167–77. https://doi.org/10.1016/0167-6423(95)00021-6.
Brady, Edwin. “SPLV20 course notes”. GitHub. https://github.com/edwinb/SPLV20