A locally nameless theory of objects
Conference paper
Henrio, L., Kammueller, F., Lutz, B. and Sudhof, H. 2010. A locally nameless theory of objects. SAFA Annual Workshop on Formal Techniques (SAFA’2010). 2229 Route des Crêtes, 06560, Valbonne, Provence-Alpes-Côte d'Azur, France
Type | Conference paper |
---|---|
Title | A locally nameless theory of objects |
Authors | Henrio, L., Kammueller, F., Lutz, B. and Sudhof, H. |
Abstract | This paper presents the formalisation of an object calculus in Isabelle/HOL highlighting the binder technique called locally nameless1. This techniques has its origins already in a note at the end of de Bruijn’s paper [5] introducing the classical de Bruijn indices. In the last few years, with the advent of mechanized proofs in the domain of programming languages, e.g. [1], this technique attracted new attention. The most recent work on locally nameless technique [2] provides cofinite quantification, necessary for proving non-trivial properties. Indeed the de Bruijn indices are often criticised, as being too technical, that is why alternative techniques are investigated. The de Bruijn indices method, however, is known to be reliable, and is often chosen in order to focus on aspects of programming languages unrelated to variable bindings. With locally nameless techniques, one expects to spend less time proving auxiliary lemmas dealing with variable bind- ings, but also to obtain theorems that are more convincing because closer to the paper version. Our contributions are a formalisation in Isabelle/HOL of ς-calculus; and an in depth comparison of both locally nameless and de Bruijn complete mechanisations including specification and proofs. |
Research Group | Foundations of Computing group |
Artificial Intelligence group | |
Conference | SAFA Annual Workshop on Formal Techniques (SAFA’2010) |
Proceedings Title | SAFA Annual Workshop on Formal Techniques (SAFA’2010) |
Publication process dates | |
Deposited | 25 May 2012 |
Output status | Published |
Web address (URL) | http://www.same-conference.org/index.php/same/same-archives/same-2010/conference/safa-workshop |
Language | English |
File |
https://repository.mdx.ac.uk/item/83q50
Download files
46
total views9
total downloads0
views this month0
downloads this month