| HAL-Inria | Publications, software ... of Inria's scientists |
Reports
A Formalization of the Theory of Objects in Isabelle/HOL
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.
Cited literature [20 references]
https://hal.inria.fr/inria-00121816
Contributor : Ludovic Henrio Connect in order to contact the contributor
Submitted on : Tuesday, February 6, 2007 - 2:48:28 PM
Last modification on : Friday, February 4, 2022 - 3:19:21 AM
Long-term archiving on: : Tuesday, September 21, 2010 - 12:36:11 PM
Contributor : Ludovic Henrio Connect in order to contact the contributor
Submitted on : Tuesday, February 6, 2007 - 2:48:28 PM
Last modification on : Friday, February 4, 2022 - 3:19:21 AM
Long-term archiving on: : Tuesday, September 21, 2010 - 12:36:11 PM
Files
RR-Sigma.pdf
Files produced by the author(s)