Email Gateway (Aug 18 2022 at 15:16): Email Gateway (Aug 18 2022 at 15:16):From: Tobias Nipkow <nipkow@in.tum.de>
http://afp.sourceforge.net/entries/Locally-Nameless-Sigma.shtml
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.
Last updated: Nov 21 2024 at 12:39 UTC