Martin Hofmann: Proof-relevant logical relations
Proof-relevant logical relations
We introduce a novel variant of logical relations that maps types not merely to partial equivalence relations on values, as is commonly done, but rather to a proof-relevant generalisation thereof, namely setoids. A setoid is like a category all of whose morphisms are isomorphisms (a groupoid) with the exception that no equations between these morphisms are required to hold. The objects of a setoid establish that values inhabit semantic types, whilst its morphisms are understood as evidence for semantic equivalence.
The transition to proof-relevance solves two well-known problems caused by the use of existential quantification over future worlds in traditional Kripke logical relations: failure of admissibility, and spurious functional dependencies.
We illustrate the novel format with two applications: a direct-style validation of Pitts and Stark's equivalences for ``new'' and a denotational semantics for a region-based effect system that supports type abstraction in the sense that only externally visible effects need to be tracked; non-observable internal modifications, such as the reorganisation of a search tree or lazy initialisation, can count as `pure' or `read only'. This `fictional purity' allows clients of a module soundly to validate more effect-based program equivalences than would be possible with traditional effect systems.
This is joint work with Nick Benton and Vivek Nigam.