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.
- 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.
- 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.
- Explorations in the untyped lambda calculus (2014)
- A simple and efficient implementation of strong call by need by an abstract machine (2022) (Code)
- Encodings for numbers in lambda calculus (2022)
- RankNTypes via Lambda Calculus (2021)
- Binary Lambda Calculus