Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Proof-relevant logical relations
Speaker:Martin Hofmann
coming from:Ludwig-Maximilians-Universitaet Muenchen
Speakers Bio:
Event Type:SWS Colloquium
Visibility:SWS, RG1
We use this to send out email in the morning.
Level:AG Audience
Date, Time and Location
Date:Monday, 13 May 2013
Duration:90 Minutes
Building:E1 5
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

Name(s):Claudia Richter
Phone:9303 9103
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:YesTo Location:Kaiserslautern
To Building:G26To Room:112
Tags, Category, Keywords and additional notes
Attachments, File(s):

Created:Claudia Richter/MPI-SWS, 05/06/2013 09:34 AM Last modified:Uwe Brahm/MPII/DE, 11/24/2016 04:14 PM
  • Claudia Richter, 05/06/2013 01:15 PM
  • Claudia Richter, 05/06/2013 09:49 AM -- Created document.