🧮 Programming with pure lambda calculus
A complete proof in Agda of the Church-Rosser theorem for untyped λ-calculus formalizing the methods by Komori-Matsuda-Yamakawa (2014) and the proof by Nagele-van Oostrom-Sternagel (2016); reuses the infrastructure for λ-terms and substitutions provided by the PLFA book
An implementation and tutorial for Lambda Calculus in Rust
Formal Verification of the 7-Color Chromatic Number of the Plane via Toroidal Projection and the Irrationality of 2π.
Some type-level magic in some languages.
Lyndon words, Duval factorization, necklace and bracelet enumeration, and De Bruijn sequences in pure Python.
Add a description, image, and links to the de-bruijn topic page so that developers can more easily learn about it.
To associate your repository with the de-bruijn topic, visit your repo's landing page and select "manage topics."