| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Locally Nameless Sigma Calculus
| Title: | Locally Nameless Sigma Calculus |
| Authors: | Ludovic Henrio (Ludovic /dot/ Henrio /at/ sophia /dot/ inria /dot/ fr), Florian Kammüller (flokam /at/ cs /dot/ tu-berlin /dot/ de), Bianca Lutz (sowilo /at/ cs /dot/ tu-berlin /dot/ de) and Henry Sudhof (hsudhof /at/ cs /dot/ tu-berlin /dot/ de) |
| Submission date: | 2010-04-30 |
| 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. |
| BibTeX: |
@article{Locally-Nameless-Sigma-AFP,
author = {Ludovic Henrio and Florian Kammüller and Bianca Lutz and Henry Sudhof},
title = {Locally Nameless Sigma Calculus},
journal = {Archive of Formal Proofs},
month = apr,
year = 2010,
note = {\url{https://isa-afp.org/entries/Locally-Nameless-Sigma.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Applicative_Lifting |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |