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
Note: We use this to send email in the morning.
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.
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 -- Created document.