lamYcalc

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:

• Locally nameless implementation in Agda

Proofs of subject invariance for intersection types:

• Locally nameless implementation in Agda