| King's Buildings, Edinburgh EH9 3JZ Scotland (2007) | |||||||||||||||||
Abstract | |||||||||||||||||
| We develop a notion of equivalence between interpretations of the simply typed -calculus together with an equationally de ned 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 -calculus to include the linear -calculus and calculi with additional type and term constructors, such as those given by sum types or by a strong monad for modelling phenomena such as partiality or nondeterminism. This is all done in terms of category theoretic structure, using -brations 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. | |||||||||||||||||
Publication details | |||||||||||||||||
| |||||||||||||||||