Paper Info
Title
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 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.
Year
DOI
Venue
2008
10.1016/j.entcs.2007.09.014
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
type-driven equivalence checking algorithm,definitional characterisation,programming languages,logical relation,isabelle/hol,equivalence checking,nominal logic work,advanced topics,case study,nominal datatype package,logical relations,formalisations,proof assistants,nominal logic work.,nominal isabelle crary,completeness proof,reasoning technique,programming language,proof assistant
Formal equivalence checking,HOL,Discrete mathematics,Logical relations,Computer science,Equivalence (measure theory),Completeness (statistics)
Journal
Volume
ISSN
Citations 
196,
Electronic Notes in Theoretical Computer Science
6
PageRank 
References 
Authors
0.60
10
2
Name
Order
Citations
PageRank
Julien Narboux113012.49
Christian Urban214212.78