Set-theoretical models of various type theories (up to an extensional version of the Calculus of Inductive Constructions), aiming at proving logical consistency and strong normalization
cmangin / cic-model-1 Goto Github PK
View Code? Open in Web Editor NEWThis project forked from barras/cic-model
Set-theoretical models of various type theories (up to an extensional version of the Calculus of Inductive Constructions), aiming at proving logical consistency and strong normalization