Lucas Lopes lucasquin
VictorTaelin
/ itt-coc.ts
Last active
August 2, 2024 16:20
ITT-Flavored Calculus of Constructions Type Checker
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| // A nano dependent type-checker featuring inductive types via self encodings. | |
| // All computation rules are justified by interaction combinator semantics, | |
| // resulting in major simplifications and improvements over old Kind-Core. | |
| // Specifically, computable annotations (ANNs) and their counterpart (ANN | |
| // binders) and a new self encoding based on equality (rather than dependent | |
| // motives) greatly reduce code size. A more complete file, including | |
| // superpositions (for optimal unification) is available on the | |
| // Interaction-Type-Theory repository. | |
| // Credits also to Franchu and T6 for insights. |