Explore λ-Abstractions Interactively

Visual λ-calculus editor with type inference, pattern matching, and interactive theorem proving.

Visual λ-Editor

Drag-and-drop node editor with β-reduction simulation and α-conversion visualization.

Hindley-Milner & dependent type analysis with visual type derivation trees.

Step-by-step natural deduction proof builder with tactic guidance.

Comprehensive guides on λ-calculus, Hindley-Milner, and dependently typed programming.

Test your functional programming skills with:

Help improve λΛ's theorem prover, editor features, or contribute to the growing collection of exercises!