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.
  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.