My Solution

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

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.