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.

Working on a polymorphic version of MirrorCore I have been working a lot with heterogeneous lists and proof-relevant membership. The later is the source of this challenge problem.

Coq provides two ways to finish definitions Qed and Defined. The former is meant for “proofs” and makes the definition opaque while the later is meant for “definitions” and leaves the definition transparent. While the “proof” and “definition” dicotomy initially makes a lot of sense to users, but as users start to use dependent types more and more, they realize that the distinction is quite arbitrary, in which case, should we abandon Qed? In this post, I argue that yes abandoning Qed is a perfectly sensible thing to do.

I spent some time experimenting with Mtac and figured that I’d write a little bit about my experience. Mtac is a tactic language for Coq where you get write Gallina terms that manipulate raw Coq syntax through a monadic interface.

You can now watch my thesis defense on computational reflection in intensional type theory. Some minor hicups during the talk but otherwise gives a very high-level overview of MirrorCore and Rtac at the time (2014).

During my post-doc at UCSD I’ve been working on verifying cyber-physical systems in the VeriDrone project. Cyber-physical systems are just systems that interact with the real world (think quadcopters, cars, planes, hydro-electric dams, and robots). The interesting thing about verifying cyber-physical systems in Coq is that they require a lot of reasoning about continuous mathematics, real numbers, differential equations, and all that. Coq does a great job at all of the discrete reasoning that we do (see my previous blog post on embedding logics in Coq) but at the end of all the nice theory, problems often boil down to mundane reasoning about real arithmetic. In this post I’m going to discuss a plugin that I wrote to call SMT solvers from Coq.

In this post I’m going to discuss Rtac the reflective tactic language that I developed as a central piece of my dissertation. The results there show how reflective tactics can be a game-changer in the ability to build very efficient automation. For comparison, the automation that I’m going to write in this post is a monoidal cancellation procedure and at the end of the post we’ll see that it scales substantially better than Ltac, e.g. on larger problems it is almost 2 orders of magnitude faster than Ltac.

Coq inductive data types are required to be strictly positive. In this article, I’ll discuss a bit about what this means, and I’ll show a simple technique to approximate an inductive data type. While not the paragon of computational efficiency, the technique that I describe here makes it possible to build inductive data types compositionally (though it only supports data-types with finite branching). In addition, it may serve as a less mathematical introduction to some of the concepts in fixpoints.

Coq comes with a powerful, built-in logic (Gallina) with features such as inductive and dependent types, recursion, etc. However, most uses of Coq don’t study its theory, but rather use it as a foundation to reason about something else. A few examples come to mind:

Computational reflection is a technique for extending proof assistants with efficient, domain-specific automation. There are a lot of interesting ideas in computational reflection but in this blog post I’m just going to cover a simple example, proving evenness of large constants. This example is purposefully extremely simple, and computational reflection is certainly capable of doing a lot more, but the very key pieces are here.