Logical Relations, Data Abstraction, and Structured Fibrations
John Power and Edmund Robinson
To appear at the 2nd International Conference on Principles and Practice of
Declarative Programming (PPDP 2000), Montreal, Canada, September 20-22, 2000
Abstract
We develop a notion of equivalence between interpretations of the
simply typed lambda-calculus together with an equationally defined
abstract data-type, and we show that two interpretations are
equivalent if and only if they are linked by a logical relation. We
show that our construction generalises from the simply typed
lambda-calculus to include the linear lambda-calculus and
calculi with additional type and term constructors, such as those
given by sum types or by a monad for modelling phenomena such as
partiality or nondeterminism. This is all done in terms of category
theoretic structure, using fibrations to model logical relations
following Hermida, and adapting Jung and Tiuryn's logical relations of
varying arity to provide the completeness results, which form the heart
of the work.