[TYPES] Paper: A Bisimulation for Type Abstraction and Recursion

[Eijiro Sumii]

Dear all,

We are pleased to announce the following paper, available at:

  http://www.cis.upenn.edu/~sumii/pub/infohide5.pdf
  http://www.cis.upenn.edu/~sumii/pub/infohide5.ps.gz
  http://www.cis.upenn.edu/~sumii/pub/infohide5.dvi

Comments are welcome.

----------------------------------------------------------------------
          A Bisimulation for Type Abstraction and Recursion

                 Eijiro Sumii and Benjamin C. Pierce

We present a sound, complete, and elementary proof method---based on
bisimulation---for contextual equivalence in lambda-calculus with full
universal, existential, and recursive types.  Unlike 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 _sets_ of relations---instead of just relations---as
bisimulations.
----------------------------------------------------------------------

Best regards,

    Eijiro Sumii
    Benjamin C. Pierce