Proofs of some theorems in lambda calculus in agda, including the Church-Rosser theorem for untyped and simply typed lambda calculus, weak normalization and strong normalization of STLC, and equivalence of SKI calculus and lambda calculus
| Name | Name | Last commit date | ||
|---|---|---|---|---|