Higher-Order refinement in Coq
and Dijkstra Specification Monads (DSM)
- proofs of programs,
functional and imperative programming, object-oriented programming.
- type theory, monads, continuations (CPS), weakest-preconditions,
- 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
This a new formulation of
- 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
- Refinement proofs are interactive: user can control in his/her proofs the way
to mix deductions (refinement rules) and computations
Contact Sylvain Boulme (please, remove underscores).
Last modification: Jun 1 2007