Intuitionistic refinement calculus

Abstract

Refinement calculi are program logics which formalize the "top-down" methodology of software development promoted by Dijkstra and Wirth in the early days of structured programming. I present here the shallow embedding of a refinement calculus into COQ constructive type theory. This embedding involves monad transformers and the computational reflexion of weakest-preconditions, using a continuation passing style. It should allow to reason about many ML programs combining non-functional features (state, exceptions, etc) with purely functional ones (higher-order functions, structural recursion, etc). © Springer-Verlag Berlin Heidelberg 2007.