lambdaex

Specification, formalization and verification of the XC function from ex lambda calculus[1]. The main work is done in xc.v file.

References

Name		Name	Last commit message	Last commit date
Latest commit History 7 Commits
.gitignore		.gitignore
Basic_Prop_lex.v		Basic_Prop_lex.v
Conclusion.v		Conclusion.v
Equation_C.v		Equation_C.v
Introduction.v		Introduction.v
Lambda.v		Lambda.v
LambdaESLab.v		LambdaESLab.v
LambdaESLab_Defs.v		LambdaESLab_Defs.v
LambdaES_Defs.v		LambdaES_Defs.v
LambdaES_FV.v		LambdaES_FV.v
LambdaES_Infra.v		LambdaES_Infra.v
LambdaES_Tac.v		LambdaES_Tac.v
Lambda_Ex.v		Lambda_Ex.v
Lambda_Int_Ext.v		Lambda_Int_Ext.v
LexSN.v		LexSN.v
LibTactics.v		LibTactics.v
Makefile		Makefile
Metatheory.v		Metatheory.v
Metatheory_Fresh.v		Metatheory_Fresh.v
Metatheory_Tactics.v		Metatheory_Tactics.v
Metatheory_Var.v		Metatheory_Var.v
NormalizationTheory.v		NormalizationTheory.v
README.md		README.md
Rewriting.v		Rewriting.v
RewritingLab.v		RewritingLab.v
SN_Properties.v		SN_Properties.v
xc.v		xc.v