Personal tools
You are here: Home Events Lab Lunch by Martin Hofmann

Lab Lunch by Martin Hofmann

Abstract effects and proof-relevant logical relations (a high-level overview)

When Nov 12, 2013
from 01:00 PM to 02:00 PM
Where MF2
Add event to calendar vCal

We give 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 to validate soundly more effect-based program  equivalences than would be possible with previous semantics. Our semantics also  lets us abstract from physical boundaries of locations. We can view an integer location as 64 boolean references that can be modified independently or spread two integer references across two physical integer locations using XOR.

The semantics uses 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.  The transition to proof-relevance solves two awkward problems caused by naive use of existential quantification in Kripke logical relations (failure of admissibility and spurious functional dependencies).

(Joint work with Nick Benton and Vivek Nigam)

Document Actions