Specification refinement with system F

Abstract

Essential concepts of algebraic specification refinement are translated into a type-theoretic setting involving System F and Reynolds' relational parametricity assertion as expressed in Plotkin and Abadi's logic for parametric polymorphism. At first order, the type-theoretic setting provides a canonical picture of algebraic specification refinement. At higher order, the type-theoretic setting allows future generalisation of the principles of algebraic specification refinement to higher order and polymorphism. We show the equivalence of the acquired type-theoretic notion of specification refinement with that from algebraic specification. To do this, a generic algebraic-specification strategy for behavioural refinement proofs is mirrored in the type-theoretic setting.