Locally Nameless Sigma Calculus

Ludovic Henrio 📧, Florian Kammüller 📧, Bianca Lutz 📧 and Henry Sudhof 📧

April 30, 2010

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session Locally-Nameless-Sigma

Depends on