| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 423733 | Electronic Notes in Theoretical Computer Science | 2008 | 16 Pages |
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
