Abstract
In this paper we present a formalization of Abadi's and Cardelli's theory of objects in the interactive theorem prover Isabelle/HOL. Our motivation is to build a mechanized HOL-framework for the analysis of a functional calculus for distributed objects. In particular, we present (a) a formal model of objects and its operational semantics based on de Bruijn 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. We expect this framework to be highly reusable and allow further development and mechanized proofs of various aspects of object theory, e.g., distribution, aspect orientation, typing. © IFIP International Federation for Information Processing 2007.
Cite
CITATION STYLE
Henrio, L., & Kammüller, F. (2007). A mechanized model of the theory of objects. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4468 LNCS, pp. 190–205). Springer Verlag. https://doi.org/10.1007/978-3-540-72952-5_12
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
