Skip to Main content Skip to Navigation
Conference papers

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

Abstract : In the book on Advanced Topics in Types and Programming Languages, Crary illustrates the reasoning method 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download

https://hal.inria.fr/inria-00180061
Contributor : Julien Narboux Connect in order to contact the contributor
Submitted on : Tuesday, June 29, 2010 - 1:50:44 PM
Last modification on : Thursday, January 6, 2022 - 11:38:04 AM
Long-term archiving on: : Thursday, December 1, 2016 - 6:09:52 AM

File

lfmtp-07.pdf
Files produced by the author(s)

Identifiers

Citation

Julien Narboux, Christian Urban. Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking.. LFMTP'07, Jul 2007, Bremen, Germany. 15p., ⟨10.1016/j.entcs.2007.09.014⟩. ⟨inria-00180061v2⟩

Share

Metrics

Record views

22

Files downloads

121