MPI-INF Logo
Campus Event Calendar

Event Entry

What and Who

A complete characterization of observational equivalence in polymorphic lambda-Calculus with general references

Eijiro Sumii
Tohoku University, Sendai, Japan
SWS Colloquium
SWS, RG1  
Expert Audience
English

Date, Time and Location

Thursday, 10 September 2009
14:00
90 Minutes
E1 5
5th floor
Saarbrücken

Abstract

We give the first sound and complete proof method for observational
equivalence in full polymorphic lambda-calculus with existential types
and first-class, higher-order references.  Our method is syntactic and
elementary in the sense that it only employs simple structures such as
relations on terms.  It is nevertheless powerful enough to prove many
interesting equivalences that can and cannot be proved by previous
approaches such as logical relations.

Contact

Claudia Richter
9325 688
--email hidden

Video Broadcast

Yes
Saarbrücken
E1 4
019
passcode not visible
logged in users only

Claudia Richter, 09/07/2009 10:47 AM -- Created document.