Lambda calculus

Is logical theory of computable functions.

Notes

Lambda calculus is a formal language capable of expressing arbitrary computable functions. In combination with types it forms a compact way to denote on the one hand functional programs and on the other hand mathematical proofs.

Lambda calculus is Turing complete, meaning you can express everything computable in a regular computer in lambda calculus.

You can formalize the entire lambda calculus inside of category theory via cartesian closed categories.

Links

Caramel - Set of bidirectional, Haskell-inspired syntax-sugars that are expanded to, and contracted from, λ-Calculus terms.

LICK - Correct-by-construction implementation of the simply-typed lamba calculus' expressions, beta-reduction, and evaluation.

Lamcal - Lambda Calculus parser and evaluator and a separate command line REPL application to play around with lambda expressions interactively.

Last modified 14d ago