[isabelle] New AFP entry: Locally Nameless Sigma Calculus


Title: Locally Nameless Sigma Calculus

Authors: Ludovic Henrio, Florian Kammüller, Bianca Lutz, Henry Sudhof

Abstract: We present a Theory of Objects based on the original
functional sigma-calculus by Abadi and Cardelli [1] 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 general Commutation.thy [4] 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 [2]. The first part, i.e. sigma-calculus confluence, has been
published on an earlier version based on lists and de Bruijn indices [3].

[1] M. Abadi and L. Cardelli. A Theory of Objects. Springer, New York, 1996.
[2] B. Aydemir, A, Charguéraud, B. C. Pierce, R. Pollack, and S. Weirich.
    Engineering formal metatheory. Princ. of Programming Languages,
    POPL'08, ACM, 2008. [3] L. Henrio and F. Kammüller. A mechanized
model of the theory of
    objects. Formal Methods for Open Object-Based Distributed Systems.
    LNCS 4468, Springer, 2007.
[4] Tobias Nipkow. More Church Rosser Proofs.
    Journal of Automated Reasoning. 26:51--66, 2001.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.