Preface
These notes attempt to provide an introduction to building models of complex programming languages in the Coq theorem prover. The topics covered extend beyond the relatively simple properties and proof techniques of progress and preservation: the goal is to show how one can use a theorem prover to build relational models of languages with complex features, such as recursive types or higher-order store.
The tutorial is intended for readers who already posess some knowledge
of semantics and interactive theorem proving. However, familiarity
with the precise techniques we are using is not necessary. More
elaboration on the prerequisites can be found in the
following. Presentation-wise, we aim for a style similar to
Pierce
Contents and Structure of the Tutorial
The Coq development that forms this tutorial and the underlying library is quite extensive and contains features outside the scope of this tutorial, at least in its current version. The tutorial aims to prepare the readers to use the libraries themselves. However, we hope one would also be able to read and understand the parts of the library the tutorial does not explain, aided with the comments and the papers that we formalise here.
The tutorial consists of three chapters. First, we attempt to familiarise the reader with the spaces we use throughout the work: the universe of complete, 1-bounded, bisected ultrametric spaces, presented here in the — perhaps more approachable — way, as complete families of equivalences. We show how to construct these objects, define the appropriate function space (the non-expansive maps), and introduce Banach's fixed-point operator for contractive maps.
The following chapters deal with building logical relations for two calculi. In Chapter 2 we show how one can use the operations on metric spaces — in particular the fixed-point operator — to model a calculus with universal and recursive types. This is still relatively simple, as the space of semantic types used can be defined directly. Finally, in Chapter 3 we tackle references (although without higher types, to keep the presentation simpler). In this chapter we use the power of the underlying library to solve a recursive domain equation and obtain the space of the semantic types — and then show how to use it to model our calculus.
As mentioned above, we do not explain the internal workings of the library. However, we invite interested readers to read through some of its code. Most of the useful abstractions used in Chapter 2 are defined in the UPred and Constr files: the definitions there should be understandable (indeed, if one is to solve all of the proposed exercises, one needs to understand the definitions in Constr). The machinery used to solve the recursive domain equation in Chapter 3 is defined in the file MetricRec. We believe it is best to understand the paper it attempts to formalise [3] before reading the formalisation itself — or at least refer to the paper while reading.
Some of the other files may be used to provide future extensions to this tutorial. In particular, in the file BI we show how some of the spaces we use form a complete BI algebra, i.e., a model of Separation Logic. This facts could be used to build a model of a Higher-Order Separation Logic with a nontrivial treatment of sharing by combining the proofs there with a solution to some recursive domain equation.
Prerequisites
There are two distinct areas the reader needs to be somewhat familiar with before attempting to read this tutorial. On one hand, some familiarity with formal semantics is needed, since the kind of interpretations discussed here are not completely straightforward. We suggest at the very least familiarity with operational semantics, polymorphism, recursive types and semantics of store as discussed in the excellent Pierce's book [1]. Particularly important is the chapter on logical relations, since this is the kind of models we will be building. Familiarity with the particular models we will be building here, as built for instance in [3], while it could certainly be helpful, is not necessary.
Since this is a rather advanced material, the reader should also have
some familiarity with the Coq system. Pierce
Exercises
We have tried to provide some exercises of varying difficulty for each of the chapters. It is our belief that, due to the sheer amount of theory operating behind the scenes, it could be quite confusing to try to use the library without attempting at least some of those. The exercises that ask the user to build binary variants of the logical relations in Chapters 2 and 3 are relatively difficult, since they would require the reader to extend some of the constructions to the binary case. We believe they could make good projects that would expose students to advanced semantic ideas and require relatively sophisticated proof engineering.
Acknowledgments
The library that forms the backbone of this tutorial has been based on an earlier formalisation by Nick Benton, Lars Birkedal, Andrew Kennedy and Carsten Varming. While both the proof engineering methods used and the scope of this library differ from their formalisation, much of the setup is borrowed from their attempt.
The tutorial also uses a version François Pottier's dblib library, which provides generic support for using DeBruijn indices, with some modifications.
Aleš Bizjak has provided a lot of discussion and code to the development of the library, in particular he modularised the construction of the solution to the recursive domain equations. Yannick Zakowski was the first user of the library, and provided an early version of the development that forms Chapter 3.