Lambda calculus

This representation is the fifth in the compilation chain (see Architecture). Its main difference with the previous default calculus is the absence of the default term, which has been eliminated through diverse compilation schemes.

The module describing the abstract syntax tree is:

• Lcalc.Ast Abstract syntax tree for the lambda calculus
• Lcalc.Print

This intermediate representation corresponds to the lambda calculus presented in the Catala formalization.

Compilation from default calculus

Lcalc.Compile_with_exceptions compiles the default term of the default calculus using catchable exceptions. This compilation scheme has been certified.

Related modules:

• Lcalc.Compile_with_exceptions Translation from the default calculus to the lambda calculus. This translation uses exceptions to handle empty default terms.

Backends

The OCaml backend of the lambda calculus is merely a syntactic formatting, since the core of the OCaml value language is effectively a lambda calculus.

Related modules:

• Lcalc.To_ocaml Formats a lambda calculus program into a valid OCaml program
• Scalc.To_python Formats a lambda calculus program into a valid Python program
• Lcalc.Backends