This is a formalization of the λ-Y calculus along with proofs of confluence (Church Rosser), formalization of intersection types for the λ-Y calculus and a proof of subject invariance for intersection types.
To download, run:
git clone --recursive https://github.com/goodlyrottenapple/lamYcalc.git
The theory files were compiled with Isabelle2016/Agda 2.5.1.
The following links point to html versions of the Isabelle/Agda theory files:
Church Rosser Theorem:
- Nominal implementation in Isabelle
- Locally nameless implementation in Isabelle
- Locally nameless implementation in Agda
Intersection types:
Proofs of subject invariance for intersection types: