Theorem-proving support in programming language semantics
Yves Bertot · Cambridge University Press eBooks · 2009
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.