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.
• To get started: try write/play with lambda calculus evaluator. Learn type theory more generally. First chapter of the HoTT book is a bit intense but not bad for this. Normalisation-by-evaluation is neat.

Links

• Dependently Typed Lambda Calculus in Haskell
• 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.
• A Gentle Introduction to Lambda Calculus - Part 1: Syntax (2018)
• Mikrokosmosai - Educational λ-calculus interpreter.
• Category Theory and Lambda Calculus (2018) (Code)
• The Impact of the Lambda Calculus (1997) [pdf] (HN)
• path - Lambda calculus to explore type-directed program synthesis.
• Fine-grain implementations of common lambda calculi in Haskell, tested with QuickCheck
• Lambda Zero - Minimalist pure lazy functional programming language.
• Dedukti - Implementation of the λΠ-calculus modulo rewriting.
• Lambda Calculus and Lambda Calculators
• pLam - Interpreter for learning and exploring pure λ-calculus.
• Y Combinator for Non-programmers: A Wild Introduction to Computer Science (Code)
• Notes on lambda calculus
• λ-calculus interpreter in less than 300 lines of JS
• Higher-order Logic and Equality (2020) (HN)
• λ-calculus ocaml library
• Simply typed lambda calculus (2020)
• The Awesome Power of Theory: Explorations in the untyped lambda calculus (2014)
• Lambda Calculus Visualizations
• History of Lambda Calculus
• Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi
• A circuit-like notation for lambda calculus (2015) (HN)
• Lambda Zoo - Implementations of different lambda calculi with abstract binding trees.
• All you need is λ, part one: booleans (2020) (HN)
• lambda-mu-mu-calculus - Interpreter for λ̅μμ̃-calculus of Herbelin and Curien.
• Notes on lambda calculus and type theory
• Fun with Lambda Calculus
• Binary Lambda Calculus
• Algorithmic Information Theory, using Binary Lambda Calculus
• Lambda calculus Notes
• Lamcal - Lambda Calculus parser and evaluator and a separate command line REPL application to play around with lambda expressions interactively.
• Lambda Calculus and Categories
• LambdaPiPlus - Simple Dependently-Typed Language for Research and Learning.
• Lambda-Calculus cooked n-ways
• lambs - Enriched typed lambda calculus.
• Lambda Calculus (2020)
• Categories and λ-calculus
• NanoHaskell - Self-hosting lambda calculus compiler.
• Fundamentals of Lambda Calculus & Functional Programming in JavaScript (2017) (Code) (Web)
• Visual Lambda Calculus Explorer
• Binary Lambda Calculus (2012) (HN)
• Simply typed lambda calculus (2020)
• Lambda Calculus Examples (2009) (HN)
• A Talk on Incremental λ-Calculus (2015)
• Simply Typed Lambda Calculus Formalization
• Viscal - Visual representation of the lambda calculus and animation of beta reduction. (Code)
• Super-Quick Lambda Calculus
• CosmicOS - Sending the lambda calculus into deep space.
• Ane-Language - Tool for analyze lambda calculus terms.
• Fibonacci sequence in JS using pure Lambda Calculus
• Lambda Calculus Visualizer (Code)
• glam - Implementation of the guarded λ-calculus.
• Formalization of Typed and Untyped λ-Calculi in Coq and Agda2
• Foundations of Dawn: The Untyped Concatenative Calculus (2021)
• λProlog interpreter
• Simpler, Easier! How to write a simple dependent type checker
• Sloe - Simple functional language based on lambda-calculus.
• Untyped Concatenative Calculus
• Categorical glueing for simply typed lambda calculus
• λ-Calculus, Combinatory Logic and Cartesian Closed Categories (2021)
• Implementing Cartesian Closed Categories - Elementary implementation of Simply Typed Lambda Calculus (STLC) and its semantics in terms of Cartesian Closed Categories.
• Compiler and runtime for normalizing the untyped λ-calculus
• ts-lambda-calc - Lambda calculus at type-level with TypeScript.
• Tiny Lazy ML with Process Calculus in plain C
• Lambda Calculus in 400 Bytes (2022) (HN)
• seq - µµ̃ calculus with pretty-printing and evaluating interpreters.
• Lambda Calculus in JS
• minitt-rs - Dependently-typed lambda calculus, Mini-TT, extended and implemented in Rust.
• λ-2D: An Exploration of Drawing as Programming Language, Featuring Ideas from Lambda Calculus (HN)
• Ultimate Calculus - Optimal, full λ-calculus evaluator that doesn't rely on interaction combinators and can be implemented in 150 lines.
• λC+ - Proof assistant based on the Calculus of Constructions.
• Simple, zero-dependency implementation of the untyped lambda calculus in Safe Rust
• Lili - Minimalist proof checker based on a simply typed lambda-calculus.
• SKI combinators - AST and Evaluating
• A DSL for λ-terms in Scala (2017)
• Binary Lambda Calculus evaluation engine written in Malbolge
• Benchmarking various normalization algorithms for the lambda calculus
• Untyped lambda calculus, written in Haskell
• Telomare - Simple total pure functional language, eventually to have powerful static checking and optimization.
• LSTS: Large Scale Type Systems - Categorical view of Typed Lambda Calculus with flexible Soundness guarantees.
• Janus - λ-calculus in Quantitative Type Theory.