Logical relations, data abstraction, and structured fibrations
John Power, E. Powell Robinson · 2000
We d e v elop a notion of equivalence between interpretations of the simply typed -calculus together with an equationally de ned abstract data-type, and we s h o w that two i n terpretations are equivalent if and only if they are linked by a logical relation.We s h o w that our construction generalises from the simply typed -calculus to include the linear -calculus and calculi with additional type and term constructors, such a s those given by s u m t ypes or by a strong monad for modelling phenomena such as partiality or nondeterminism.This is all done in terms of category theoretic structure, usingbrations 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.