Translations of a lambda abstraction to combinations of operators, with proofs written in Coq.
Closure_calculus contains the variant of lambda-calculus. SF-calculus contains SF calculus (see also the repository SF). Fieska-calculus augments SF-calculus with more operators. Closure_to_Fieska translates closure calculus to Fieska-calculus. Closure_to_SF translates closure calculus to SF-calculus.
Tree_calculus introduces tree calculus. The main theorems are:
- translation_preserves_sf_reduction
- translation_preserves_abs_reduction
- eager_is_definable
_CoqProject and the make files and script are all out of date.