[TYPES/announce] two bisimulation papers

[Eijiro Sumii]

Dear Types readers,

I am pleased to announce the availability of the following two manuscripts:

----------------------------------------------------------------------

A Complete Characterization of Observational Equivalence in
Polymorphic lambda-Calculus with General References

                              Eijiro Sumii

  http://www.kb.ecei.tohoku.ac.jp/~sumii/pub/poly-ref.pdf

We give a (sound and complete) characterization of 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, including the latest work by Ahmed,
Dreyer and Rossberg (to appear in POPL 2009).

----------------------------------------------------------------------

A Higher-Order, Call-By-Value Applied Pi-Calculus

          Nobuyuki Sato          Eijiro Sumii

  http://www.kb.ecei.tohoku.ac.jp/~sumii/pub/hoapp.pdf

We define a higher-order process calculus with algebraic operations
such as encryption and decryption, and develop a bisimulation proof
method for behavioral equivalence in this calculus.  Such development
has been notoriously difficult because of the subtle interactions
among generative names, processes as data, and the algebraic
operations.  We handle them by carefully defining the calculus and
adopting Sumii et al.'s environmental bisimulation, and thereby give
(to our knowledge) the first ``useful'' proof method in this setting.
We demonstrate the utility of our method through examples involving
both higher-order processes and asymmetric cryptography.

----------------------------------------------------------------------

Comments are welcome.

Cheers,

       Eijiro