Locally nameless sigma calculus
Article
Henrio, L., Kammueller, F., Lutz, B. and Sudhof, H. 2010. Locally nameless sigma calculus. Archive of Formal Proof.
Type | Article |
---|---|
Title | Locally nameless sigma calculus |
Authors | Henrio, L., Kammueller, F., Lutz, B. and Sudhof, H. |
Abstract | We present a Theory of Objects based on the original functional sigma-calculus by Abadi and Cardelli but with an additional parameter to methods. We prove confluence of the operational semantics following the outline of Nipkow's proof of confluence for the lambda-calculus reusing his theory Commutation, a generic diamond lemma reduction. We furthermore formalize a simple type system for our sigma-calculus including a proof of type safety. The entire development uses the concept of Locally Nameless representation for binders. We reuse an earlier proof of confluence for a simpler sigma-calculus based on de Bruijn indices and lists to represent objects. |
Research Group | Foundations of Computing group |
Artificial Intelligence group | |
Journal | Archive of Formal Proof |
ISSN | 2150-914X |
Publication dates | |
30 Apr 2010 | |
Publication process dates | |
Deposited | 25 May 2012 |
Output status | Published |
Web address (URL) | http://afp.sourceforge.net/entries/Locally-Nameless-Sigma.shtml |
Language | English |
Permalink -
https://repository.mdx.ac.uk/item/83q4z
35
total views0
total downloads0
views this month0
downloads this month