Skip to Main content Skip to Navigation
Reports

A Formalization of the Theory of Objects in Isabelle/HOL

Ludovic Henrio 1 Florian Kammüller 2
1 OASIS - Active objects, semantics, Internet and security
CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : We present a formalization of Abadi's and Cardelli's theory of objects in the interactive theorem prover Isabelle/HOL. In particular, we present (a) a formal model of objects and its operational semantics based on DeBruijn indices (b) a parallel reduction relation for objects (c) the proof of confluence for the theory of objects reusing Nipkow's HOL-framework for the lambda calculus.
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/inria-00121816
Contributor : Ludovic Henrio <>
Submitted on : Tuesday, February 6, 2007 - 2:48:28 PM
Last modification on : Tuesday, May 26, 2020 - 6:50:22 PM
Document(s) archivé(s) le : Tuesday, September 21, 2010 - 12:36:11 PM

Files

RR-Sigma.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00121816, version 2

Collections

Citation

Ludovic Henrio, Florian Kammüller. A Formalization of the Theory of Objects in Isabelle/HOL. [Research Report] RR-6079, INRIA. 2006, pp.17. ⟨inria-00121816v2⟩

Share

Metrics

Record views

369

Files downloads

231