Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking

In the book on Advanced Topics in Types and Programming Languages, Crary illustrates the reasoning technique of logical relations in a case study about equivalence checking. He presents a type-driven equivalence checking algorithm and verifies its completeness with respect to a definitional characterisation of equivalence. We present in this paper a formalisation of Crary's proof using Isabelle/HOL and the nominal datatype package.

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Julien Narboux, Christian Urban
• Keywords: ENTCS 2008, Logical Relations, Nominal Datatype Package, Type-driven Equivalence