My Solution

This is my solution to the challenge problem posted elsewhere. It's decomposed into a series of modules:

Source code tarball

  • Binding, a piece of a general library for reasoning about dependently-typed abstract syntax trees and Debruijn indices. This is very sparsely commented. I recommend skipping over it at first; the interesting parts about it should be clear from seeing how it's used later.
  • PSLC, the syntax and semantics of the simply typed lambda calculus with products and sums. Syntax and static semantics are combined via dependently-typed ASTs, and the dynamic semantics is given as a denotational semantics translating terms of the source language into "native" Coq terms.
  • MemMonad, a generic monad for writing imperative programs in Coq, in the tradition of the Haskell IO monad. This module also contains a modest decision procedure (in the form of a Coq tactical script) for goals involving specifications for monadic values.
  • Imp, the syntax and semantics of the imperative target language. Static semantics is again by dependently-typed ASTs, and dynamic semantics is by compilation into monadic Coq programs.
  • Programs, some small examples of proving correctness properties of programs in both languages.
  • ImpCompile, the compiler and its proof of semantics preservation, via a logical relations argument.
  • You can also see the OCaml code for the real compiler extracted from the Coq development.

    General warnings about the Coq source: This development requires the -impredicative-set Coq flag, and it depends on a single extra axiom: proof irrelevance for propositional equality.