zbMATH — the first resource for mathematics

Formal certification of a resource-aware language implementation. (English) Zbl 1252.68070
Berghofer, Stefan (ed.) et al., Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-03358-2/pbk). Lecture Notes in Computer Science 5674, 196-211 (2009).
Summary: The paper presents the development, by using the proof assistant Isabelle/HOL, of a compiler back-end translating from a functional source language to the bytecode language of an abstract machine. The Haskell code of the compiler is extracted from the Isabelle/HOL specification and this tool is also used for proving the correctness of the implementation. The main correctness theorem not only ensures functional semantics preservation but also resource consumption preservation: the heap and stacks figures predicted by the semantics are confirmed in the translation to the abstract machine.
The language and the development belong to a wider proof-carrying code framework in which formal compiler-generated certificates about memory consumption are sought for.
For the entire collection see [Zbl 1173.68002].

68N20 Theory of compilers and interpreters
68N18 Functional programming and lambda calculus
68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI
[1] Dold, A., Vialard, V.: A Mechanically Verified Compiling Specification for a Lisp Compiler. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 144–155. Springer, Heidelberg (2001) · Zbl 1052.68584 · doi:10.1007/3-540-45294-X_13
[2] Barthe, G., Grégoire, B., Kunz, C., Rezk, T.: Certificate Translation for Optimizing Compilers. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 301–317. Springer, Heidelberg (2006) · Zbl 1225.68062 · doi:10.1007/11823230_20
[3] Berghofer, S., Strecker, M.: Extracting a formally verified, fully executable compiler from a proof assistant. In: Proc. Compiler Optimization Meets Compiler Verification, COCV 2003. ENTCS, pp. 33–50 (2003)
[4] Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004) · doi:10.1007/978-3-662-07964-5
[5] Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a C compiler front-end. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 460–475. Springer, Heidelberg (2006) · Zbl 05289024 · doi:10.1007/11813040_31
[6] Dave, M.A.: Compiler verification: a bibliography. SIGSOFT Software Engineering Notes 28(6), 2 (2003) · doi:10.1145/966221.966235
[7] Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: Proc. 30th ACM Symp. on Principles of Programming Languages, POPL 2003, pp. 185–197. ACM Press, New York (2003) · Zbl 1321.68180
[8] Klein, G., Nipkow, T.: Verified Bytecode Verifiers. Theoretical Computer Science 298, 583–626 (2003) · Zbl 1038.68109 · doi:10.1016/S0304-3975(02)00869-1
[9] Klein, G., Nipkow, T.: A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler. ACM Transactions on Programming Languages and Systems 28(4), 619–695 (2006) · doi:10.1145/1146809.1146811
[10] Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Principles of Programming Languages, POPL 2006, pp. 42–54. ACM Press, New York (2006) · Zbl 1369.68124
[11] Leroy, X.: A formally verified compiler back-end, July 2008, p. 79 (submitted, 2008) · Zbl 1185.68215
[12] Li, G., Owens, S., Slind, K.: Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 205–219. Springer, Heidelberg (2007) · Zbl 1187.68141 · doi:10.1007/978-3-540-71316-6_15
[13] Lindholm, T., Yellin, F.: The Java Virtual Machine Sepecification, 2nd edn. The Java Series. Addison-Wesley, Reading (1999)
[14] Montenegro, M., Peña, R., Segura, C.: A Resource-Aware Semantics and Abstract Machine for a Functional Language with Explicit Deallocation. In: Workshop on Functional and (Constraint) Logic Programming, WFLP 2008, Siena, Italy, July 2008, pp. 47–61 (2008) (to appear in ENTCS) · Zbl 1347.68054
[15] Montenegro, M., Peña, R., Segura, C.: A Simple Region Inference Algorithm for a First-Order Functional Language. In: Trends in Functional Programming, TFP 2008, Nijmegen (The Netherlands), May 2008, pp. 194–208 (2008)
[16] Montenegro, M., Peña, R., Segura, C.: A Type System for Safe Memory Management and its Proof of Correctness. In: ACM Principles and Practice of Declarative Programming, PPDP 2008, Valencia, Spain, July 2008, pp. 152–162 (2008) · doi:10.1145/1389449.1389468
[17] Montenegro, M., Peña, R., Segura, C.: An Inference Algorithm for Guaranteeing Safe Destruction. In: LOPSTR 2008. LNCS, vol. 5438, pp. 135–151. Springer, Heidelberg (2009) · Zbl 1185.68200 · doi:10.1007/978-3-642-00515-2_10
[18] Necula, G.C.: Proof-Carrying Code. In: ACM SIGPLAN-SIGACT Principles of Programming Languages, POPL 1997, pp. 106–119. ACM Press, New York (1997)
[19] Necula, G.C.: Translation validation for an optimizing compiler. SIGPLAN Notices 35(5), 83–94 (2000) · doi:10.1145/358438.349314
[20] Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL. A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002) · Zbl 0994.68131 · doi:10.1007/3-540-45949-9
[21] Peña, R., Rupérez, D.: A Certified Implementation of a Functional Virtual Machine on top of the Java Virtual Machine. In: Jornadas sobre Programación y Lenguajes, PROLE 2008, Gijón, Spain, October 2008, pp. 131–140 (2008)
[22] Peña, R., Segura, C., Montenegro, M.: A Sharing Analysis for SAFE. In: Selected Papers of the 7th Symp. on Trends in Functional Programming, TFP 2006, pp. 109–128 (2007) (Intellect)
[23] Pnueli, A., Siegel, M., Singerman, E.: Translation Validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 151–166. Springer, Heidelberg (1998) · doi:10.1007/BFb0054170
[24] Sannela, D., Hofmann, M.: Mobile Resources Guarantees. EU Open FET project, IST 2001-33149 2001-2005, http://www.dcs.ed.ac.uk/home/mrg
[25] Strecker, M.: Formal Verification of a Java Compiler in Isabelle. In: Voronkov, A. (ed.) CADE 2002. LNCS, vol. 2392, pp. 63–77. Springer, Heidelberg (2002) · Zbl 1072.68593 · doi:10.1007/3-540-45620-1_5
[26] Wildmoser, M.: Verified Proof Carrying Code. Ph.D. thesis, Institut für Informatik, Technical University Munchen (2005)
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.