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.
_CoqProject and the make files should (re-)construct the proofs. If there are problems, consult the script.