Paper: Eager Normal Form Bisimulation (at LICS 2005)

Authors: Soren B. Lassen

Abstract

This paper describes two new bisimulation equivalences for the pure untyped call-by-value ?-calculus, called enf bisimilarity and enf bisimilarity up to ?. They are based on eager reduction of terms to eager normal form (enf), analogously to co-inductive bisimulation characterizations of Lévy-Longo tree equivalence and Böhm tree equivalence (up to ?). We argue that enf bisimilarity is the call-by-value analogue of Lévy-Longo tree equivalence. Enf bisimilarity (up to ?) is the congruence on source terms induced by the call-by-value CPS transform and Böhm tree equivalence (up to ?) on target terms. Enf bisimilarity and enf bisimilarity up to ? enjoy powerful bisimulation proof principles which, among other things, can be used to establish a retraction theorem for the call-by-value CPS transform.

BibTeX

  @InProceedings{Lassen-EagerNormalFormBisi,
    author = 	 {Soren B. Lassen},
    title = 	 {Eager Normal Form Bisimulation},
    booktitle =  {Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005)},
    year =	 {2005},
    month =	 {June}, 
    pages =      {345--354},
    location =   {Chicago, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }