Title: Refinement calculus & Martin-Lof type theory

Abstract:
"The refinement calculus [of Back, von Wright et al.] is an elegant
 quasi-algebraic formalism for refining imperative specifications to
 executable programs.  The standard interpretation of its "contract"
 expressions is as predicate transformers acting on predicates over a
 state-space; it is usually given in classical, impredicative higher
 order logic.  ML type theory is a family of type theories based on
 the idea that proofs and effective constructions are programs,
 propositions are types, and predicates are data-dependent types.  It
 supports inductive definitions and reflection principles of various
 kinds, but is entirely constructive and predicative.

 The talk concerns a straightforward interpretation of contract
 expressions as certain data structures in Martin-Lof type theory.
 The structures were first described by Petersson and Synek, and are
 dependent types par excellence; these can be used to effectively
 model imperative, command-response interfaces. This suggests, modulo
 some foundational issues in ML TT connected with coinduction and
 singleton predicates, a logical form for specifications of both
 client-side "transaction" programs (that terminate), as well as
 server programs (that run forever)."