Abstract
The formal verification of compilers and related programming tools depends crucially on the availability of appropriate mechanized semantics for the source, intermediate and target languages. In this invited talk, I review various forms of operational semantics and their mechanization, based on my experience with the formal verification of the CompCert C compiler.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
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
Milner, R.: Communication and Concurrency. Prentice-Hall (1990)
Milner, R.: Communicating and Mobile Systems: the pi-Calculus. Cambridge University Press (1999)
Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115(1), 38–94 (1994)
Aydemir, B.E., Charguéraud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: 35th symposium Principles of Programming Languages, pp. 3–15. ACM Press (2008)
Appel, A.W., McAllester, D.A.: An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems 23(5), 657–683 (2001)
Danielsson, N.A.: Operational semantics using the partiality monad. In: International Conference on Functional Programming 2012, pp. 127–138. ACM Press (2012)
Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM 52(7), 107–115 (2009)
Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd Symposium Principles of Programming Languages, pp. 42–54. ACM Press (2006)
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)
Leroy, X.: A formally verified compiler back-end. Journal of Automated Reasoning 43(4), 363–446 (2009)
Leroy, X., Grall, H.: Coinductive big-step operational semantics. Information and Computation 207(2), 284–304 (2009)
Appel, A.W., Blazy, S.: Separation Logic for Small-Step cminor. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 5–21. Springer, Heidelberg (2007)
Felleisen, M., Friedman, D.P.: Control operators, the SECD machine and the λ-calculus. In: Formal Description of Programming Concepts III, pp. 131–141. North-Holland (1986)
Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science 410(46), 4747–4768 (2009)
Curien, P.-L., Munch-Maccagnoni, G.: The Duality of Computation under Focus. In: Calude, C.S., Sassone, V. (eds.) TCS 2010. IFIP AICT, vol. 323, pp. 165–181. Springer, Heidelberg (2010)
Benton, N., Hur, C.K.: Biorthogonality, step-indexing and compiler correctness. In: International Conference on Functional Programming 2009, pp. 97–108. ACM Press (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leroy, X. (2012). Mechanized Semantics for Compiler Verification. In: Hawblitzel, C., Miller, D. (eds) Certified Programs and Proofs. CPP 2012. Lecture Notes in Computer Science, vol 7679. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35308-6_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-35308-6_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35307-9
Online ISBN: 978-3-642-35308-6
eBook Packages: Computer ScienceComputer Science (R0)