Skip to content
/ cic-model Public

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

2 stars 2 forks Branches Tags Activity
Star
Notifications You must be signed in to change notification settings

barras/cic-model

BranchesTags

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

204 Commits
broken
broken
 
 
graph
graph
 
 
template
template
 
 
tests
tests
 
 
.depend
.depend
 
 
.depend-html
.depend-html
 
 
.gitignore
.gitignore
 
 
AbsSNT.v
AbsSNT.v
 
 
AbsTheoryIntp.v
AbsTheoryIntp.v
 
 
AbsTheorySem.v
AbsTheorySem.v
 
 
AbsTheorySyn.v
AbsTheorySyn.v
 
 
CCTnat.v
CCTnat.v
 
 
CCUT.v
CCUT.v
 
 
Can.v
Can.v
 
 
Choice.v
Choice.v
 
 
Conv.v
Conv.v
 
 
ConvECC.v
ConvECC.v
 
 
Ens.v
Ens.v
 
 
EnsEm.v
EnsEm.v
 
 
EnsEmUniv.v
EnsEmUniv.v
 
 
EnsLogic.v
EnsLogic.v
 
 
EnsUniv.v
EnsUniv.v
 
 
EnsZ.v
EnsZ.v
 
 
Env.v
Env.v
 
 
EnvECC.v
EnvECC.v
 
 
Explicit_sub.v
Explicit_sub.v
 
 
FOTheory.v
FOTheory.v
 
 
GenLemmas.v
GenLemmas.v
 
 
GenModel.v
GenModel.v
 
 
GenModelNat.v
GenModelNat.v
 
 
GenModelSN.v
GenModelSN.v
 
 
GenModelSyntax.v
GenModelSyntax.v
 
 
GenRealSN.v
GenRealSN.v
 
 
HF.v
HF.v
 
 
HFcoc.v
HFcoc.v
 
 
HFrelation.v
HFrelation.v
 
 
InstInterp.v
InstInterp.v
 
 
InstSem.v
InstSem.v
 
 
InstSyn.v
InstSyn.v
 
 
IntMap.v
IntMap.v
 
 
Lambda.v
Lambda.v
 
 
Logics.v
Logics.v
 
 
Makefile
Makefile
 
 
ModelCC.v
ModelCC.v
 
 
ModelCC_em.v
ModelCC_em.v
 
 
ModelECC.v
ModelECC.v
 
 
ModelECCW_sized.v
ModelECCW_sized.v
 
 
ModelECC_oldstyle.v
ModelECC_oldstyle.v
 
 
ModelHF.v
ModelHF.v
 
 
ModelNat.v
ModelNat.v
 
 
ModelNat_ZFind.v
ModelNat_ZFind.v
 
 
ModelNat_sized.v
ModelNat_sized.v
 
 
ModelTheory.v
ModelTheory.v
 
 
ModelZF.v
ModelZF.v
 
 
Model_variance.v
Model_variance.v
 
 
Models.v
Models.v
 
 
MyList.v
MyList.v
 
 
Nest.v
Nest.v
 
 
NonUniform.v
NonUniform.v
 
 
ObjectSN.v
ObjectSN.v
 
 
PIntp.v
PIntp.v
 
 
PSem.v
PSem.v
 
 
PSyn.v
PSyn.v
 
 
README.md
README.md
 
 
SATnat.v
SATnat.v
 
 
SATnat_real.v
SATnat_real.v
 
 
SATtypes.v
SATtypes.v
 
 
SATw.v
SATw.v
 
 
SN_CC.v
SN_CC.v
 
 
SN_CC_Real.v
SN_CC_Real.v
 
 
SN_CC_Real_syntax.v
SN_CC_Real_syntax.v
 
 
SN_ECC.v
SN_ECC.v
 
 
SN_ECC_Real.v
SN_ECC_Real.v
 
 
SN_ECC_Real_syntax.v
SN_ECC_Real_syntax.v
 
 
SN_NAT.v
SN_NAT.v
 
 
SN_NAT_sized.v
SN_NAT_sized.v
 
 
SN_P.v
SN_P.v
 
 
SN_Theory.v
SN_Theory.v
 
 
SN_W.v
SN_W.v
 
 
SN_nat.v
SN_nat.v
 
 
SN_ord.v
SN_ord.v
 
 
SN_variance.v
SN_variance.v
 
 
Sat.v
Sat.v
 
 
SnModels.v
SnModels.v
 
 
StrengthenECC.v
StrengthenECC.v
 
 
Sublogic.v
Sublogic.v
 
 
Term.v
Term.v
 
 
TermECC.v
TermECC.v
 
 
TheoryInTerm.v
TheoryInTerm.v
 
 
TypModels.v
TypModels.v
 
 
TypeECC.v
TypeECC.v
 
 
TypeJudge.v
TypeJudge.v
 
 
TypeJudgeECC.v
TypeJudgeECC.v
 
 
Types.v
Types.v
 
 
VarMap.v
VarMap.v
 
 
ZF.v
ZF.v
 
 
ZFcoc.v
ZFcoc.v
 
 
ZFcofix.v
ZFcofix.v
 
 
ZFcoll.v
ZFcoll.v
 
 
ZFcont.v
ZFcont.v
 
 

Repository files navigation

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

About

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

Resources

Readme
Activity

Stars

2 stars

Watchers

2 watching

Forks

2 forks
Report repository

Releases

No releases published

Packages

No packages published

Languages