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


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.