[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  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  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 . The first part, i.e. sigma-calculus confluence, has been
published on an earlier version based on lists and de Bruijn indices .
 M. Abadi and L. Cardelli. A Theory of Objects. Springer, New York, 1996.
 B. Aydemir, A, Charguéraud, B. C. Pierce, R. Pollack, and S. Weirich.
Engineering formal metatheory. Princ. of Programming Languages,
POPL'08, ACM, 2008.  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.
 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