Lambda calculus
Is logical theory of computable functions.
• 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.

• 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.
• minitt-rs - Rust implementation of Mini-TT, a simple dependently-typed lambda calculus.
• Mikrokosmosai - Educational λ-calculus interpreter.
• path - Lambda calculus to explore type-directed program synthesis.
• Lambda Zero - Minimalist pure lazy functional programming language.
• Dedukti - Implementation of the λΠ-calculus modulo rewriting.
• pLam - Interpreter for learning and exploring pure λ-calculus.
• Lambda Zoo - Implementations of different lambda calculi with abstract binding trees.
• lambda-mu-mu-calculus - Interpreter for λ̅μμ̃-calculus of Herbelin and Curien.
• Lamcal - Lambda Calculus parser and evaluator and a separate command line REPL application to play around with lambda expressions interactively.
• LambdaPiPlus - Simple Dependently-Typed Language for Research and Learning.
• lambs - Enriched typed lambda calculus.
• NanoHaskell - Self-hosting lambda calculus compiler.
• Viscal - Visual representation of the lambda calculus and animation of beta reduction. (Code)
• CosmicOS - Sending the lambda calculus into deep space.
• Ane-Language - Tool for analyze lambda calculus terms.
• glam - Implementation of the guarded λ-calculus.
• Sloe - Simple functional language based on lambda-calculus.
• Implementing Cartesian Closed Categories - Elementary implementation of Simply Typed Lambda Calculus (STLC) and its semantics in terms of Cartesian Closed Categories.