Thumbnail
Access Restriction
Subscribed

Author Sumii, Eijiro ♦ Pierce, Benjamin C.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©2007
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Lambda-calculus ♦ Bisimulations ♦ Contextual equivalence ♦ Existential types ♦ Logical relations ♦ Recursive types
Abstract We present a bisimulation method for proving the contextual equivalence of packages in λ-calculus with full existential and recursive types. Unlike traditional logical relations (either semantic or syntactic), our development is “elementary,” using only sets and relations and avoiding advanced machinery such as domain theory, admissibility, and TT-closure. Unlike other bisimulations, ours is complete even for existential types. The key idea is to consider $\textit{sets}$ of relations—instead of just relations—as bisimulations.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2007-10-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 54
Issue Number 5


Open content in new tab

   Open content in new tab
Source: ACM Digital Library