Normalization for a combinatorial presentation of Gödel's system T using a gleuing model construction.
This mechanization is primarily based on the paper Intuitionistic model constructions and normalization proofs by Coquand and Dybjer.
nachivpn/gluetn
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|