Skip to content
/ lambdaSF Public
forked from Barry-Jay/lambdaSF

implementation of lambda-SF-calculus plus some basic theorems

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

bondi-lang/lambdaSF

BranchesTags
 
 

Folders and files

NameName
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

About

implementation of lambda-SF-calculus plus some basic theorems

Resources

Readme
Activity
Custom properties

Stars

0 stars

Watchers

1 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

No packages published

Languages

  • Coq 100.0%