×

zbMATH — the first resource for mathematics

A mechanized model of the theory of objects. (English) Zbl 1202.68097
Bonsangue, Marcello M. (ed.) et al., Formal methods for open object-based distributed systems. 9th IFIP WG 6.1 international conference FMOODS 2007, Paphos, Cyprus, June 6–8, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72919-8/pbk). Lecture Notes in Computer Science 4468, 190-205 (2007).
Summary: 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.
For the entire collection see [Zbl 1118.68002].

MSC:
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68N18 Functional programming and lambda calculus
68Q55 Semantics in the theory of computing
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abadi, M., Cardelli, L.: A Theory of Objects. Springer, New York (1996) · Zbl 0876.68014
[2] Abadi, M., Cardelli, L.: A Theory of Primitive Objects. DEC Research Labs, TR (1995) · Zbl 0942.03523
[3] Abadi, M., Cardelli, L.: An imperative object calculus. In: Mosses, P.D., Schwartzbach, M.I., Nielsen, M. (eds.) CAAP 1995, FASE 1995, and TAPSOFT 1995. LNCS, vol. 915, Springer, Heidelberg (1995)
[4] Barendregt, H.P.: The Lambda Calculus, its Syntax and Semantics, 2nd edn. North-Holland, Amsterdam (1984) · Zbl 0551.03007
[5] Briais, S., Nestmann, U.: Mobile objects must move safely. In: Formal Methods for Open Object-Based Distributed Systems IV. Proceedings of FMOODS’2002, University of Twente, the Netherlands, Kluwer Academic Publishers, Dordrecht (2002) · Zbl 1048.68026
[6] Niehren, J., Schwinghammer, J., Smolka, G.: A concurrent lambda calculus with futures. Theoretical Computer Science 364(3), 338–356 (2006) · Zbl 1110.68023
[7] de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae 34, 381–392 (1972) · Zbl 0253.68007
[8] Berghofer, S., Urban, C.: A Head-to-Head Comparison of de Bruijn Indices and Names. In: Head-to-Head, A. (ed.) LFMTP 2006. Proceedings of the International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice. ENTCS, Elsevier, Amsterdam (2006) · Zbl 1278.03033
[9] Di Blasio, P., Fisher, K.: A calculus for concurrent objects. In: International Conference on Concurrency Theory (1996)
[10] Cardelli, L.: A language with distributed scope. In: POPL’95. Conference Record of the 22nd ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (1995)
[11] Caromel, D., Henrio, L.: A Theory of Distributed Objects. Springer, Heidelberg (2005) · Zbl 1084.68012
[12] Caromel, D., Henrio, L., Serpette, B.P.: Asynchronous and deterministic objects. In: Proceedings of the 31st ACM SIGACT-SIGPLAN symposium on Principles of programming languages, ACM Press, New York (2004) · Zbl 1325.68052
[13] Ciaffaglione, A., Liquori, L., Miculan, M.: Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts. Journal of Automated Reasoning (to appear, 2007) · Zbl 1118.68046
[14] Ehmety, S.O.: Theory of objects in Isabelle/ZF. Unpublished theory files (1999)
[15] Gordon, A.D., Hankin, P.D.: A concurrent object calculus: reduction and typing. In: concurrent, A. (ed.) Proceedings HLCL’98. ENTCS, vol. 16, Elsevier, Amsterdam (1998) · Zbl 0917.68064
[16] Gordon, A.D., Rees, G.D.: Bisimilarity for a first-order calculus of objects with subtyping. In: POPL’96. Conference Record of the 23rd ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, ACM Press, New York (1996)
[17] Jähnichen, S., Kammüller, F.: Ascot: Formal, mechanical foundation of aspect-oriented and collaboration-based languages. Project with the German Research Foundation (DFG) (2006)
[18] Kammüller, F.: Author’s web-page (2006), http://swt.cs.tu-berlin.de/ flokam
[19] Ligatti, J., Walker, D., Zdancewic, S.: A type-theoretic interpretation of pointcuts and advice. In: Science of Computer Programming: Special Issue on Foundations of Aspect-Oriented Programming, Springer, Heidelberg (2006) · Zbl 1119.68112
[20] Nipkow, T.: More Church Rosser Proofs. Journal of Automated Reasoning 26, 51–66 (2001) · Zbl 0958.03011
[21] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
[22] Pierce, B.C., Turner, D.N.: Concurrent objects in a process calculus. In: Ito, T., Yonezawa, A. (eds.) TPPP 1994. LNCS, vol. 907, Springer, Heidelberg (1995)
[23] Urban, C., et al.: Nominal Methods Group. Project funded by the German Research Foundation (DFG) within the Emmy-Noether Programme (2006), Web-page at http://www4.in.tum.de/ urbanc/Nominal/
[24] Urban, C., Tasson, C.: Nominal Techniques in Isabelle/HOL. In: Nieuwenhuis, R. (ed.) Automated Deduction – CADE-20. LNCS (LNAI), vol. 3632, Springer, Heidelberg (2005) · Zbl 1135.68561
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.