Name		Name	Last commit message	Last commit date
Latest commit History 12 Commits
Lambda		Lambda
Beta_Reduction.glob		Beta_Reduction.glob
Beta_Reduction.v		Beta_Reduction.v
Beta_Reduction.vo		Beta_Reduction.vo
Binding.glob		Binding.glob
Binding.v		Binding.v
Binding.vo		Binding.vo
Combinators.glob		Combinators.glob
Combinators.v		Combinators.v
Combinators.vo		Combinators.vo
Equal.glob		Equal.glob
Equal.v		Equal.v
Equal.vo		Equal.vo
Eta.glob		Eta.glob
Eta.v		Eta.v
Eta.vo		Eta.vo
Extensional_to_combinator.glob		Extensional_to_combinator.glob
Extensional_to_combinator.v		Extensional_to_combinator.v
Extensional_to_combinator.vo		Extensional_to_combinator.vo
General.glob		General.glob
General.v		General.v
General.vo		General.vo
Homomorphism.glob		Homomorphism.glob
Homomorphism.v		Homomorphism.v
Homomorphism.vo		Homomorphism.vo
Intensional_to_combinator.glob		Intensional_to_combinator.glob
Intensional_to_combinator.v		Intensional_to_combinator.v
Intensional_to_combinator.vo		Intensional_to_combinator.vo
LamSF_Closed.glob		LamSF_Closed.glob
LamSF_Closed.v		LamSF_Closed.v
LamSF_Closed.vo		LamSF_Closed.vo
LamSF_Confluence.glob		LamSF_Confluence.glob
LamSF_Confluence.v		LamSF_Confluence.v
LamSF_Confluence.vo		LamSF_Confluence.vo
LamSF_Cube.glob		LamSF_Cube.glob
LamSF_Cube.v		LamSF_Cube.v
LamSF_Cube.vo		LamSF_Cube.vo
LamSF_Eval.glob		LamSF_Eval.glob
LamSF_Eval.v		LamSF_Eval.v
LamSF_Eval.vo		LamSF_Eval.vo
LamSF_Marks.glob		LamSF_Marks.glob
LamSF_Marks.v		LamSF_Marks.v
LamSF_Marks.vo		LamSF_Marks.vo
LamSF_Normal.glob		LamSF_Normal.glob
LamSF_Normal.v		LamSF_Normal.v
LamSF_Normal.vo		LamSF_Normal.vo
LamSF_Redexes.glob		LamSF_Redexes.glob
LamSF_Redexes.v		LamSF_Redexes.v
LamSF_Redexes.vo		LamSF_Redexes.vo
LamSF_Residuals.glob		LamSF_Residuals.glob
LamSF_Residuals.v		LamSF_Residuals.v
LamSF_Residuals.vo		LamSF_Residuals.vo
LamSF_Simulation.glob		LamSF_Simulation.glob
LamSF_Simulation.v		LamSF_Simulation.v
LamSF_Simulation.vo		LamSF_Simulation.vo
LamSF_Substitution.glob		LamSF_Substitution.glob
LamSF_Substitution.v		LamSF_Substitution.v
LamSF_Substitution.vo		LamSF_Substitution.vo
LamSF_Substitution_term.glob		LamSF_Substitution_term.glob
LamSF_Substitution_term.v		LamSF_Substitution_term.v
LamSF_Substitution_term.vo		LamSF_Substitution_term.vo
LamSF_Tactics.glob		LamSF_Tactics.glob
LamSF_Tactics.v		LamSF_Tactics.v
LamSF_Tactics.vo		LamSF_Tactics.vo
LamSF_Terms.glob		LamSF_Terms.glob
LamSF_Terms.v		LamSF_Terms.v
LamSF_Terms.vo		LamSF_Terms.vo
LamSF_reduction.glob		LamSF_reduction.glob
LamSF_reduction.v		LamSF_reduction.v
LamSF_reduction.vo		LamSF_reduction.vo
Lambda_tactics.v		Lambda_tactics.v
Primitive_Recursion.v		Primitive_Recursion.v
README.md		README.md
SF_reduction.glob		SF_reduction.glob
SF_reduction.v		SF_reduction.v
SF_reduction.vo		SF_reduction.vo
Test.glob		Test.glob
Test.v		Test.v
Test.vo		Test.vo
Unstar.glob		Unstar.glob
Unstar.v		Unstar.v
Unstar.vo		Unstar.vo
script		script

Repository files navigation

lambdaSF

implementation of lambda-SF-calculus plus some basic theorems, such as confluence

Barry-Jay/lambdaSF

Folders and files

Latest commit

History