×

zbMATH — the first resource for mathematics

Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts. (English) Zbl 1118.68046
Summary: We illustrate a methodology for formalizing and reasoning about Abadi and Cardelli’s object-based calculi, in (co)inductive type theory, such as the calculus of (co)inductive constructions, by taking advantage of natural deduction semantics and coinduction in combination with weak higher-order abstract syntax and the theory of contexts. Our methodology allows us to implement smoothly the calculi in the target metalanguage; moreover, it suggests novel presentations of the calculi themselves. In detail, we present a compact formalization of the syntax and semantics for the functional and the imperative variants of the \(\varrho\)-calculus. Our approach simplifies the proof of subject deduction theorems, which are proved formally in the proof assistant Coq with a relatively small overhead.

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
KRAKATOA; Coq
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Berlin Heidelberg New York (1996) · Zbl 0876.68014
[2] Barendregt, H., Nipkow, T. (eds.): In: Proceedings of TYPES. Lecture Notes in Computer Science, vol. 806 (1994) · Zbl 0825.00120
[3] Bertot, Y.: A certified compiler for an imperative language. Technical Report RR-3488, INRIA (1998)
[4] Bucalo, A., Hofmann, M., Honsell, F., Miculan, M., Scagnetto, I.: Consistency of the theory of contexts. J. Funct. Program. 16(3), 327–395 (2006) · Zbl 1092.68022
[5] Burstall, R., Honsell, F.: Operational semantics in a natural deduction setting. In: Huet, G., Plotkin, G. (eds.) Logical Frameworks, pp. 185–214. Cambridge University Press (1990) · Zbl 0755.03011
[6] Cardelli, L.: Obliq: a language with distributed scope. Comput. Syst. 8(1), 27–59 (1995)
[7] Cervesato, I., Pfenning, F.: A linear logical framework. Inf. Comput. 179(1), 19–75 (2002) · Zbl 1031.03056
[8] Chirimar, J.L.: Proof theoretic approach to specification languages. Ph.D. thesis, University of Pennsylvania (1995)
[9] Ciaffaglione, A.: Certified reasoning on real numbers and objects in co-inductive type theory. Ph.D. thesis, Dipartimento di Matematica e Informatica, Università di Udine, Italy and INPL-ENSMN, Nancy, France (2003)
[10] Ciaffaglione, A., Liquori, L., Miculan, M.: Imperative object-calculi in (Co)inductive type theories. In: Proceedings of LPAR. Lecture Notes in Computer Science, vol. 2850. Springer, Berlin Heidelberg New York (2003) · Zbl 1273.03105
[11] Ciaffaglione, A., Liquori, L., Miculan, M.: Reasoning on an imperative object-calculus in higher-order abstract syntax. In: [30], ACM (2003) · Zbl 1273.03105
[12] Ciaffaglione, A., Liquori, L., Miculan, M.: The web appendix of this paper. University of Udine, Italy. http://www.dimi.uniud.it/ciaffagl (2003) · Zbl 1118.68046
[13] Ciaffaglione, A., Scagnetto, I.: Plug and play the theory of contexts in higher-order abstract syntax. In: Proceedings of CoMeta (2003) · Zbl 1271.68084
[14] Coq: The Coq Proof Assistant 7.3. INRIA. http://coq.inria.fr (2003)
[15] Crole, R.L.: Lectures on [Co]induction and [Co]algebras. Technical Report 1998/12, Department of Mathematics and Computer Science, University of Leicester (1998)
[16] Despeyroux, J.: Proof of translation in natural semantics. In: Proceedings of LICS, pp. 193–205, ACM (1986)
[17] Despeyroux, J., Felty, A., Hirschowitz, A.: Higher-order syntax in Coq. In: Proceedings of TLCA. Lecture Notes in Computer Science, vol. 905. Springer, Berlin Heidelberg New York (1995) · Zbl 1063.68650
[18] Despeyroux, J., Leleu, P.: Recursion over objects of functional type. Math. Struct. Comput. Sci. 11(4), 555–572 (2001) · Zbl 1116.03306
[19] Felty, A.P.: Two-level meta-reasoning in Coq. In: Carreño, V., Muñoz, C., Tashar, S. (eds.) Proceedings of TPHOLs. Lecture Notes in Computer Science, vol. 2410, pp. 198–213. Springer, Berlin Heidelberg New York (2002) · Zbl 1013.68201
[20] Fiore, M.P., Plotkin, G.D., Turi, D.: Abstract syntax and variable binding. In: [37], pp. 193–202. IEEE Computer Society Press (1999)
[21] Fisher, K., Honsell, F., Mitchell, J.: A lambda calculus of objects and method specialization. Nord. J. Comput. 1, 3–37 (1994) · Zbl 0886.03010
[22] Frost, J.: A case study of co-induction in Isabelle. Technical Report 359, University of Cambridge, Computer Laboratory. Revised version of CUCL 308, August 1993 (1995)
[23] Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Form. Asp. Comput. 13, 341–363 (2002) · Zbl 1001.68083
[24] Gillard, G.: A formalization of a concurrent object calculus up to alpha-conversion. In: Proceedings of CADE 17, pp. 417–432. Springer, Berlin Heidelberg New York (2000) · Zbl 0963.68033
[25] Giménez, E.: Codifying guarded recursion definitions with recursive schemes. In: Smith, J. (ed.) Proceedings of TYPES. Lecture Notes in Computer Science, vol. 996, pp. 39–59. Springer, Berlin Heidelberg New York (1995)
[26] Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of ACM 40(1), 143–184 (1993) · Zbl 0778.03004
[27] Hofmann, M.: Semantical analysis of higher-order abstract syntax. In: [37], pp. 204–213. IEEE Computer Society Press (1999)
[28] Hofmann, M., Tang, F.: Implementing a program logic of objects in a higher-order logic theorem prover. In: Proceedings of TPHOLs, pp. 268–282 (2000) · Zbl 0974.68185
[29] Hofmann, M., Tang, F.: A higher-order embedding of a logic of objects. Technical Report EDI-INF-RR-0033, LFCS, University of Edinburgh (2001)
[30] Honsell, F., Miculan, M., Momigliano, A. (eds.): Eighth ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding, MERLIN 2003. ACM (2003)
[31] Honsell, F., Miculan, M., Scagnetto, I.: An axiomatic approach to metareasoning on systems in higher-order abstract syntax. In: Proceedings of ICALP. Lecture Notes in Computer Science, vol. 2076, pp. 963–978 (2001) · Zbl 0986.68016
[32] Honsell, F., Miculan, M., Scagnetto, I.: {\(\pi\)}-calculus in (Co)inductive type theory. Theor. Comp. Sci. 253(2), 239–285 (2001) · Zbl 0956.68095
[33] Huisman, M.: Reasoning about Java programs in higher order logic with PVS and Isabelle. Ph.D. thesis, Katholieke Universiteit Nijmegen (2001)
[34] Kahn, G.: Natural semantics. In: Proceedings of STACS. Lecture Notes in Computer Science, vol. 247, pp. 22–39. Springer, Berlin Heidelberg New York (1987) · Zbl 0635.68007
[35] Klein, G., Nipkow, T.: Verified bytecode verifiers. Theor. Comp. Sci. 298(3), 583–626 (2003) · Zbl 1038.68109
[36] Laurent, O.: Sémantique naturelle et Coq: vers la spécification et les preuves sur les langages à objets. Technical Report RR-3307, INRIA (1997)
[37] Longo, G. (ed.): Proceedings of LICS. IEEE Computer Society Press (1999)
[38] Marché, C., Paulin-Mohring, C., Urbain, X.: The KRAKATOA: a tool for certification of JAVA/JAVACARD programs annotated in JML. Journal of Logic and Algebraic Programming 58(1-2), 89–106 (2004) · Zbl 1073.68678
[39] McDowell, R., Miller, D.: A logic for reasoning with higher-order abstract syntax. In: Proceedings of 12 th LICS, pp. 434–445 (1997)
[40] Miculan, M.: The expressive power of structural operational semantics with explicit assumptions. In: [2], pp. 292–320 (1994)
[41] Miculan, M.: Encoding logical theories of programs. Ph.D. thesis, Dipartimento di Informatica, Università di Pisa, Italy (1997)
[42] Miculan, M.: Developing (meta)theory of lambda-calculus in the theory of contexts. In: Ambler, S., Crole, R., Momigliano, A. (eds.) Proceedings of MERLIN ENTCS, vol. 58.1, pp. 1–22. Elsevier (2001) · Zbl 1268.68050
[43] Miculan, M.: On the formalization of the modal {\(\mu\)}-calculus in the calculus of inductive constructions. Inf. Comput. 164(1), 199–231 (2001) · Zbl 1007.03032
[44] Miller, D.: A multiple-conclusion meta-logic. In: Abramsky, S. (ed.) Proceedings of LICS. Paris, pp. 272–281 (1994)
[45] Milner, R., Tofte, M.: Co-induction in relational semantics. Theor. Comp. Sci. 87, 209–220 (1991) · Zbl 0755.68100
[46] Momigliano, A., Ambler, S.: Multi-level meta-reasoning with higher order abstract syntax. In: Proceedings of FOSSACS. Springer, Berlin Heidelberg New York (2003) · Zbl 1029.68043
[47] Norrish, M.: Mechanising Hankin and Barendregt using the Gordon–Melham axioms. In: [30], ACM (2003)
[48] Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proceedings of ACM SIGPLAN ’88 Symposium on Language Design and Implementation, pp. 199–208 (1988)
[49] Scagnetto, I.: Reasoning about names in higher-order abstract syntax. Ph.D. thesis, Dipartimento di Matematica e Informatica, Università di Udine, Italy (2002)
[50] Scagnetto, I., Miculan, M.: Ambient calculus and its logic in the calculus of inductive constructions. In: Pfenning, F. (ed.) Proceedings of LFM. Electronic Notes in Theoretical Computer Science, vol. 70.2. Elsevier (2002) · Zbl 1270.03052
[51] Self: The Self programming language. Sun Microsystems. http://research.sun.com/self/language.html (2003)
[52] Strecker, M.: Formal verification of a Java compiler in Isabelle. In: Proceedings of CADE. Lecture Notes in Computer Science, vol. 2392, pp. 63–77. Springer, Berlin Heidelberg New York (2002) · Zbl 1072.68593
[53] Tews, H.: A case study in coalgebraic specification: memory management in the FIASCO microkernel. Technical report, TU Dresden (2000)
[54] Van den Berg, J., Jacobs, B., Poll, E.: Formal specification and verification of JavaCard’s Application Identifier Class. In: Proceedings of the JavaCard 2000 Workshop (2001) · Zbl 0980.68685
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.