Proof-relevant logical relations

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