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.

DescriptionThis 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

ContactSylvain Boulme (please, remove underscores).

Last modification: Jun 1 2007