Skip to main content Accessibility help

We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.

Close cookie message
×
Hostname: page-component-66644f4456-gqvjv Total loading time: 0 Render date: 2025-02-13T02:38:29.610Z Has data issue: true hasContentIssue false

15 - Theorem-proving support in programming language semantics

Published online by Cambridge University Press:  06 August 2010

By
Yves Bertot
Edited by
Yves Bertot ,
Gérard Huet ,
Jean-Jacques Lévy  and
Gordon Plotkin
Yves Bertot
Affiliation:
INRIA Sophia-Antipolis Méditerranée
Yves Bertot
Affiliation:
INRIA-Sophia Antipolis, France
Gérard Huet
Affiliation:
Institut National de Recherche en Informatique et en Automatique (INRIA), Rocquencourt
Jean-Jacques Lévy
Affiliation:
Institut National de Recherche en Informatique et en Automatique (INRIA), Rocquencourt
Gordon Plotkin
Affiliation:
University of Edinburgh
Get access

Summary

Abstract

We describe how the formal description of a programming language can be encoded in the Coq theorem prover. Four aspects are covered: Natural semantics (as advocated by Gilles Kahn), axiomatic semantics, denotational semantics, and abstract interpretation. We show that most of these aspects have an executable counterpart and describe how this can be used to support proofs about programs.

Introduction

Nipkow demonstrated in that theorem provers could be used to formalize many aspects of programming language semantics. In this paper, we want to push the experiment further to show that this formalization effort also has a practical outcome, in that it makes it possible to integrate programming tools inside theorem provers in an uniform way. We re-visit the study of operational, denotational semantics, axiomatic semantics, and weakest pre-condiction calculus as already studied by Nipkow and we add a small example of a static analysis tool based on abstract interpretation.

To integrate the programming tools inside the theorem prover we rely on the possibility to execute the algorithms after they have been formally described and proved correct, a technique known as reflection. We also implemented a parser, so that the theorem prover can be used as a playground to experiment on sample programs. We performed this experiment using the Coq system. The tools that are formally described can also be “extracted” outside the proof environment, so that they become stand alone programs.

Type
Chapter
Information
From Semantics to Computer Science
Essays in Honour of Gilles Kahn
 , pp. 337 - 362
Publisher: Cambridge University Press
Print publication year: 2009

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

[1]B. E., Aydemir, A., Bohannon, M., Fairbairn, J. N., Foster, B. C., Pierce, P., Sewell, D., Vytiniotis, G., Washburn, S., Weirich and S., Zdancewic. Mechanized metatheory for the masses: The POPLmark challenge. In Proceedings of the Eighteenth International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), pp. 50–65. Springer-Verlag, 2005.Google Scholar
[2]G., Barthe, G., Dufay, L., Jakubiec, S., Melo de Sousa and B., Serpette. A formal executable semantics of the JavaCard platform. In D., Sands (ed.) Proceedings of ESOP'01, volume 2028 Lecture Notes in Computer Science, pp. 302–319. Springer-Verlag, 2001.Google Scholar
[3]G., Barthe, M., Ruys and H., Barendregt. A two-level approach towards lean proof-checking. In TYPES '95: Selected papers from the International Workshop on Types for Proofs and Programs, London, UK, pp. 16–35. Springer-Verlag, 1996.Google Scholar
[4]S., Berghofer and T., Nipkow. Executing higher order logic. In P., Callaghan, Z., Luo, J., McKinna and R., Pollack (eds) TYPES, volume 2277, Lecture Notes in Computer Science, pp. 24–40. Springer-Verlag, 2000.Google Scholar
[5]Y., Bertot. A Certified Compiler for an Imperative Language. Research Report RR-3488, INRIA, 1998.Google Scholar
[6]Y., Bertot. Formalizing a jvml verifier for initialization in a theorem prover. In Computer Aided Verification (CAV'2001), volume 2102, Lecture Notes in Computer Science, pp. 14–24. Springer-Verlag, 2001.Google Scholar
[7]Y., Bertot. A survey of semantics styles, 2007. available on the Coq site at coq.inria.fr/Semantics_survey.html.
[8]Y., Bertot and P., Castéran. Interactive Theorem Proving and Program Development, Coq'Art:the Calculus of Inductive Constructions. Springer-Verlag, 2004.Google Scholar
[9]Y., Bertot and R., Fraer. Reasoning with executable specifications. In TAPSOFT'95, volume 915, Lecture Notes in Computer Science, pp. 531–545, 1995.Google Scholar
[10]P., Borras, D., Clément, T., Despeyroux, J., Incerpi, G., Kahn, B., Lang and V., Pascual. Centaur: the system. In Third Symposium on Software Development Environments, 1988.Google Scholar
[11]S., Boutin. Using reflection to build efficient and certified decision procedures. In Theoretical Aspects of Computer Science, volume 1281, Lecture Notes in Computer Science, pp. 515–529. Springer-Verlag, 1997.Google Scholar
[12]A., Chaieb. Proof-producing program analysis. In K., Barkaoui, A., Cavalcanti and A., Cerone (eds) ICTAC, volume 4281, Lecture Notes in Computer Science, pp. 287–301. Springer-Verlag, 2006.Google Scholar
[13]R., Constable, S. F., Allen, H. M., Bromley, W. R., Cleaveland, J. F., Cremer, R. W., Harber, D. J., Howe, T. B., Knoblock, N. P., Mendler, P., Panangaden, J. T., Sasaki and S.F., Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986.Google Scholar
[14]C., Coquand. Agda. www.cs.chalmers.se/∼catarina/agda.
[15]P., Cousot and R., Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pp. 238–252, Los Angeles, California, 1977. ACM Press, New York, NY.Google Scholar
[16]E. W., Dijkstra. A discipline of Programming. Prentice Hall, 1976.Google Scholar
[17]G., Dowek, A., Felty, H., Herbelin, G., Huet, C., Murthy, C., Parent, C., Paulin-Mohring and B., Werner. The Coq Proof Assistant User's Guide. INRIA, May 1993. Version 5.8.Google Scholar
[18]J.-C., Filliâtre. Proof of imperative programs in type theory. In International Workshop TYPES'98, volume 1657, Lecture Notes in Computer Science, pp. 78–92. Springer-Verlag, March 1998.Google Scholar
[19]M. J. C., Gordon and T. F., Melham. Introduction to HOL : a theorem-proving environment for higher-order logic. Cambridge University Press, 1993.Google Scholar
[20]M. J. C., Gordon, R., Milner and C. P., Wadsworth. Edinburgh LCF, volume 78, Lecture Notes in Computer Science. Springer-Verlag, 1979.Google Scholar
[21]C. A. R., Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12:576–580, 1969.Google Scholar
[22]G., Kahn. Natural semantics. In K., Fuchi and M., Nivat (eds) Programming of Future Generation Computers, pp. 237–258. North-Holland, 1988. (also appears as INRIA Report no. 601).Google Scholar
[23]P., Letouzey. A new extraction for Coq. In H., Geuvers and F., Wiedijk (eds) TYPES 2002, volume 2646, Lecture Notes in Computer Science, pp. 200–219. Springer-Verlag, 2003.Google Scholar
[24]O., Müller, T., Nipkow, D., von Oheimb and O., Slotosch. HOLCF = HOL + LCF. Journal of Functional Programming, 9:191–223, 1999.Google Scholar
[25]T., Nipkow. Winskel is (almost) right: Towards a mechanized semantics. Formal Asp. Computing, 10(2):171–186, 1998.Google Scholar
[26]L. C., Paulson and T., Nipkow. Isabelle : a Generic Theorem Prover, volume 828, Lecture Notes in Computer Science. Springer-Verlag, 1994.Google Scholar
[27]D., Pichardie. Interprétation abstraite en logique intuitionniste : extraction d'analyseurs Java certifiés. PhD thesis, Université Rennes 1, 2005. (In French).
[28]G., Plotkin. Structural operational semantics. Lecture notes DAIMI FN-19, Aarhus University, 1981. (reprinted 1991).
[29]D., Terrasse. Encoding natural semantics in Coq. In Proceedings of the Fourth International Conference on Algebraic Methodology and Software Technology, AMAST'95, Lecture Notes in Computer Science, pp. 230–244. Springer-Verlag, 1995.Google Scholar
[30]J., van den Berg and B., Jacobs. The loop compiler for Java and JML. In TACAS 2001, pp. 299–312. Springer-Verlag, 2001.Google Scholar
[31]D. von, Oheimb. Analyzing Java in Isabelle/HOL, Formalization, Type Safety, and Hoare Logic. PhD thesis, Technische Universität München, 2000.
[32]G., Winskel. The Formal Semantics of Programming Languages, an introduction. Foundations of Computing. The MIT Press, 1993.Google Scholar

Save book to Kindle

To save this book to your Kindle, first ensure [email protected] is added to your Approved Personal Document E-mail List under your Personal Document Settings on the Manage Your Content and Devices page of your Amazon account. Then enter the ‘name’ part of your Kindle email address below. Find out more about saving to your Kindle.

Note you can select to save to either the @free.kindle.com or @kindle.com variations. ‘@free.kindle.com’ emails are free but can only be saved to your device when it is connected to wi-fi. ‘@kindle.com’ emails can be delivered even when you are not connected to wi-fi, but note that service fees apply.

Find out more about the Kindle Personal Document Service.

Available formats
×

Save book to Dropbox

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Dropbox.

Available formats
×

Save book to Google Drive

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Google Drive.

Available formats
×