Theorem proving support in programming language semantics

TL;DR

This paper presents a comprehensive framework for formalizing and verifying various semantics of a simple programming language within the Coq proof system, enabling integrated proof and analysis capabilities.

Contribution

It introduces formalized natural, denotational, axiomatic, and abstract semantics in Coq, along with verified tools like interpreters and analyzers derived from these semantics.

Findings

All semantics are formally proved sound within Coq.

A verified static analyzer and verification condition generator are implemented.

An interpreter is extracted from the denotational semantics.

Abstract

We describe several views of the semantics of a simple programming language as formal documents in the calculus of inductive constructions that can be verified by the Coq proof system. Covered aspects are natural semantics, denotational semantics, axiomatic semantics, and abstract interpretation. Descriptions as recursive functions are also provided whenever suitable, thus yielding a a verification condition generator and a static analyser that can be run inside the theorem prover for use in reflective proofs. Extraction of an interpreter from the denotational semantics is also described. All different aspects are formally proved sound with respect to the natural semantics specification.