Skip to content

cmangin/cic-model-1

BranchesTags
 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

173 Commits
broken
broken
 
 
graph
graph
 
 
template
template
 
 
.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
 
 
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
 
 
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
 
 
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
 
 
ZFcard.v
ZFcard.v
 
 
ZFcoc.v
ZFcoc.v
 
 
ZFcoll.v
ZFcoll.v
 
 
ZFcont.v
ZFcont.v
 
 
ZFdef.v
ZFdef.v
 
 
ZFecc.v
ZFecc.v
 
 
ZFfix.v
ZFfix.v
 
 
ZFfixfun.v
ZFfixfun.v
 
 
ZFfixrec.v
ZFfixrec.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

0 stars

Watchers

1 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

 
 
 

Contributors

Languages

  • Rocq Prover 99.5%
  • Other 0.5%