Skip to content

Latest commit

 

History

History
10 lines (9 loc) · 486 Bytes

README.md

File metadata and controls

10 lines (9 loc) · 486 Bytes

PER model for System T

This repository contains a mechanized PER model for Gödel's System T (call-by-name variant) in Coq. The relational model is more powerful than the predicate model since it allows one to prove that $\lambda x. x$ and $\lambda x . x + 0$ are logically equivalent functions from Nat to Nat.

I find it slightly trickier to mechanize call-by-name version than the call-by-value version since the base case for the Nat type becomes slightly more complicated.