In my last post I presented an implementation of a fixpoint combinator in Coq. In this post, I’m going to show how that technique can be used to give a compositional denotational semantics to Imp, a simple imperative programming language. I’m not going to pretend to cover all the corner cases of C in this post (perhaps a future post), but rather will focus on the general recipe for defining semantics using co-inductive effects.

There have been several different articles that advocate for the use of denotational semantics, where we give a function from the syntax to another language that we already understand. In Coq, the target language is often Gallina. However, because all Gallina programs terminate, we can’t give a direct interpretation of non-terminating programs. An alternative is to give a denotation of your source language through a co-inductive definition of traces. The problem with this is that co-recursion is notoriously non-compositional in Coq. The paco work provides a compositional proof rule for co-inductive types, but the is no similar definition for co-inductive definitions. In this post I’m going to explain how to build a general recursion combinator in Coq that is completely composable- a surprisingly difficult problem that I pondered for a while in grad school.

There is a tension between being too strongly (statically) typed and too weakly (statically) typed. In this post, I show how to use existential types to “derive” untyped syntax from typed syntax. This allows you to use strongly typed syntax and selectively escape to an untyped world, e.g. to do parsing or non-local transformations, without needing to maintain two different syntax definitions. This solution arose as part of discussions with Matthew Farkas-Dyck, Daniel Winograd-Cort, Moritz Drexl, and the problem was originally posed to me by Daniel King.

In this post I’m going to discuss a problem that I ran into while working with shape indexed types in Haskell and an elgant solution that is inspired by dependent type theory. The problem is implementing functions that produce values of shape-indexed types without accepting a value to do case analysis on in order to refine the index. A simple example arrises when implementing an Applicative instance for length indexed vectors.

One of the biggest complaints about proof assistants such as Coq is performance. Large proofs can be slow to both construct and to check which reduces the “interactive” nature of interactive proof assistants and makes maintenance painful. However, while the richness of dependent type theory is partially to blame for this slowness, it also allows us to use computational reflection to extend the proof checker to build and check proofs quickly. In computational reflection, we convert proof objects in to computations and run them on Coq’s bytecode virtual machine to achieve orders of magnitude improvements in proof construction and checking. In this talk I walk through how computational reflection works using a few small examples. Time permitting, I will discuss how these ideas can be used to build larger scale reflective automation (the MirrorCore project) including an Ltac-like DSL for reflective automation that provides some of the speed benefits of computational reflection without some of the drawbacks.