Abstract
This paper presents a compiler which produces machine code from functions defined in the logic of a theorem prover, and at the same time proves that the generated code executes the source functions. Unlike previously published work on proof-producing compilation from a theorem prover, our compiler provides broad support for user-defined extensions, targets multiple carefully modelled commercial machine languages, and does not require termination proofs for input functions. As a case study, the compiler is used to construct verified interpreters for a small LISP-like language. The compiler has been implemented in the HOL4 theorem prover.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
The Netwide Assembler, http://www.nasm.us/
The GNU Project. GCC, the GNU Compiler Collection, http://gcc.gnu.org/
Benton, N., Zarfaty, U.: Formalizing and verifying semantic type soundness of a simple compiler. In: Leuschel, M., Podelski, A. (eds.) Principles and Practice of Declarative Programming (PPDP), pp. 1–12. ACM, New York (2007)
Cheney, C.J.: A non-recursive list compacting algorithm. Commun. ACM 13(11), 677–678 (1970)
Chlipala, A.J.: A certified type-preserving compiler from lambda calculus to assembly language. In: Programming Language Design and Implementation (PLDI), pp. 54–65. ACM, New York (2007)
Crary, K., Sarkar, S.: Foundational certified code in a metalogical framework. Technical Report CMU-CS-03-108, Carnegie Mellon University (2003)
Fox, A.: Formal specification and verification of ARM6. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 25–40. Springer, Heidelberg (2003)
Gordon, M., Iyoda, J., Owens, S., Slind, K.: Automatic formal synthesis of hardware from higher order logic. Electr. Notes Theor. Comput. Sci. 145, 27–43 (2006)
Guttman, J., Ramsdell, J., Wand, M.: VLISP: A verified implementation of scheme. Lisp and Symbolic Computation 8(1/2), 5–32 (1995)
Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Trans. Program. Lang. Syst. 28(4), 619–695 (2006)
Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Principles of Programming Languages (POPL), pp. 42–54. ACM Press, New York (2006)
Li, G.-D., 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)
Li, G.-D., Slind, K.: Compilation as rewriting in higher order logic. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol. 4603, pp. 19–34. Springer, Heidelberg (2007)
Li, G., Slind, K.: Trusted source translation of a total function language. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 471–485. Springer, Heidelberg (2008)
Meyer, T., Wolff, B.: Tactic-based optimized compilation of functional programs. In: Filliâtre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 201–214. Springer, Heidelberg (2006)
Myreen, M.O., Fox, A.C.J., Gordon, M.J.C.: A Hoare logic for ARM machine code. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 272–286. Springer, Heidelberg (2007)
Myreen, M.O., Gordon, M.J.C.: A Hoare logic for realistically modelled machine code. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 568–582. Springer, Heidelberg (2007)
Myreen, M.O., Slind, K., Gordon, M.J.C.: Machine-code verification for multiple architectures – An application of decompilation into logic. In: Formal Methods in Computer Aided Design (FMCAD). IEEE, Los Alamitos (2008)
Necula, G.C.: Translation validation for an optimizing compiler. In: Programming Language Design and Implementation (PLDI), pp. 83–94. ACM, New York (2000)
Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 151–166. Springer, Heidelberg (1998)
Rinard, M.C.: Credible compilation. In: Jähnichen, S. (ed.) CC 1999. LNCS, vol. 1575. Springer, Heidelberg (1999)
Tristan, J.-B., Leroy, X.: Formal verification of translation validators: a case study on instruction scheduling optimizations. In: Principles of Programming Languages (POPL), pp. 17–27. ACM, New York (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Myreen, M.O., Slind, K., Gordon, M.J.C. (2009). Extensible Proof-Producing Compilation. In: de Moor, O., Schwartzbach, M.I. (eds) Compiler Construction. CC 2009. Lecture Notes in Computer Science, vol 5501. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00722-4_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-00722-4_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00721-7
Online ISBN: 978-3-642-00722-4
eBook Packages: Computer ScienceComputer Science (R0)