The choice of how you encode something has a big impact on how well the development will scale. What works well for pencil-and-paper isn't necessarily the right way to structure things in a Coq development. Here, we see a number of ways to encode the semantics of a programming language and discuss the tradeoffs, at least when we're doing shallow reasoning (e.g., type soundness).
At the same time, we'll identify a couple of key principles for scalable Coq development:
What does it mean for a compiler front-end (i.e., lexer and parser) to be correct? This turns out to be a trickier issue than it first appears. And existing tools (e.g., Yacc, Lex) aren't as usefully declarative as they appear.
In the first part, we'll focus on regular expressions and building a certified matcher, based on derivatives. This turns out to be relatively simple, beautiful, and reasonably efficient when compared to naive backtracking-based approaches.
In the second part, we'll focus on not only matching, but extracting semantic values as we match a regular expression. Here, we take advantage of indexed types to make sure that our semantic actions remain type-correct in spite of transformations like taking the derivative. We'll also consider how to define a (conservative) notion of computable equality on data structures that may have functions embedded within them and see that this is possible, though we have to jump through some major hoops.
The Coq sources for this lecture are SimpleLex.v, LexParser.v, and LexParser2.v.
The corresponding Coqdoc files are SimpleLex.html, LexParser.html, and LexParser2.html.
Sometimes, you have to convince Coq that a function terminates and the metric isn't a straightforward structural induction. Here, we'll examine unification in the context of a type-inference routine, see how the occurs check is a crucial part of the termination argument, and how we can use dependent types to ensure unification does terminate.
We'll also see shades of imperative programming, as we have to track a set of constraints on type variables when we do type- inference.
The Coq sources for this lecture are Inference.v and the corresponding Coqdoc is Inference.html.
In the first part, we'll show how we can do a shallow embedding of Hoare logic into Coq, and how the use of a higher-order logic greatly simplifies the calculation of pre- and post-conditions. This is a generally useful trick for doing imperative programming in Coq.
In the second part, we'll discuss why Hoare logic doesn't really provide for modular reasoning and how ideas like separation logic can help.
The Coq sources (so far) for this lecture are HTT0.v and Sep.v and the corresponding Coqdocs are HTT0.html and Sep.html.