Higher-Order refinement in Coq
and Dijkstra Specification Monads (DSM)

Keywords

• proofs of programs, functional and imperative programming, object-oriented programming.
• type theory, monads, continuations (CPS), weakest-preconditions, predicate transformers.

Objectives

• Defining a formal specification language for proving programs mixing purely functional features (higher-order functions, pattern-matching, structural recursion) and impure features (side-effects, exception handling, non-determinism). Typically, Objective Caml programs.
• Implementing an interactive assistant to build refinement proofs in Coq.

Description This a new formulation of refinement calculus. Main characteristics:

• Functions (i.e. parameterized specifications) are values.
• The core logic is intuitionistic type theory (instead of classical logics). More precisely, it is Coq. This allows to have functions as values.
• The specification language is an expression language (instead of a statement language). It is a monad.
• Computational reflexion of weakest-precondition calculus. Structural recursion and pattern-matching are embedded into the wp-calculus.
• Refinement proofs are interactive: user can control in his/her proofs the way to mix deductions (refinement rules) and computations (wp-simplifications).

To download

• Intuitionistic Refinement Calculus an extended version of In Proc. of International Conference on Typed Lambda Calculi and Applications (TLCA 2007), LNCS 4583, Springer-Verlag, Paris, June 2007. This extended version is examplified on the modelization of the Nim game. Execution of the game is modelized as a higher-order imperative function, parametrized by the actions of players. These actions are described as imperative non-deterministic specifications.
• a 3-pages document: Higher-order imperative enumeration of binary trees in Coq (Mar 14 2007). This document illustrates proofs in the state monad fragment of the state DSM.
• a first prototype of DSM library in Coq (coq V8.1 sources. Mar 14 2007)
• a very preliminary (but very detailed) draft: (version Feb 22 2006)
  Specifying and reasoning in Coq with high-order impure programs using specifications a la Dijkstra and refinement.

Links

• This work has begun as part of Geccoo project.
• My home page

Contact Sylvain Boulme (please, remove underscores).