Yves Bertot: Type-theoretic functional semantics

• Defines a little imperative language IMP (from [Winskel 1993]).
• Gives an operational semantics, represented as an inductively defined relation in Coq.
• Gives a denotational semantics, represented as functions in Coq. Resolves problems with general recursion and nontermination.
• Formally proves that the operational semantics is equivalent to the functional semantics.
• Extracts an interpreter (as OCaml code) from the denotational semantics.