A complete characterization of observational equivalence in polymorphic λ-calculus with general references

Research output: Chapter in Book/Report/Conference proceedingConference contribution

30 Citations (Scopus)

Abstract

We give the first sound and complete proof method for observational equivalence in full polymorphic λ-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, including the latest work by Ahmed, Dreyer and Rossberg (POPL 2009).

Original languageEnglish
Title of host publicationComputer Science Logic - 23rd International Workshop, CSL 2009 - 18th Annual Conference of the EACSL, Proceedings
Pages455-469
Number of pages15
DOIs
Publication statusPublished - 2009 Nov 2
Event23rd International Workshop on Computer Science Logic, CSL 2009 - 18th Annual Conference of the EACSL - Coimbra, Portugal
Duration: 2009 Sep 72009 Sep 11

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5771 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other23rd International Workshop on Computer Science Logic, CSL 2009 - 18th Annual Conference of the EACSL
CountryPortugal
CityCoimbra
Period09/9/709/9/11

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A complete characterization of observational equivalence in polymorphic λ-calculus with general references'. Together they form a unique fingerprint.

  • Cite this

    Sumii, E. (2009). A complete characterization of observational equivalence in polymorphic λ-calculus with general references. In Computer Science Logic - 23rd International Workshop, CSL 2009 - 18th Annual Conference of the EACSL, Proceedings (pp. 455-469). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5771 LNCS). https://doi.org/10.1007/978-3-642-04027-6_33