Links und Funktionen

Sie sind hier: Startseite / Lehre / SS 2013 / Oberseminar / Martin Hofmann: Proof-relevant logical relations


Martin Hofmann: Proof-relevant logical relations

TCS Oberseminar, 17.05.2013, 14:15 Uhr L109
Wann 14:15 15:15 17.05.2013
von bis
Wo L109
Termin übernehmen vCal

Martin Hofmann
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.



abgelegt unter: