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.
Domains
Programming Languages [cs.PL]
Origin : Files produced by the author(s)
Loading...