This repository contains implementations of the BUBS algorithm.
It can normalize any term from the pure untyped λ-calculus (including open terms).
The algorithm was invented by Olin Shivers and Mitchell Wand, who have written a research paper about it:
- https://dl.acm.org/doi/10.5555/1922521.1922535
- https://www.ccs.neu.edu/home/shivers/papers/bubs.pdf
- https://www.ccs.neu.edu/home/wand/papers/shivers-wand-10.pdf
Copying welcome.
All original work is public domain.