Logic in Computer Science (LICS 1993)

Paper: A coinduction principle for recursive data types based on bisimulation (at LICS 1993)

Authors: Marcelo P. Fiore

Abstract

The concept of bisimulation from concurrency theory is used to reason about recursively defined data types. From two strong-extensionality theorems stating that the equality (resp. inequality) relation is maximal among all bisimulations, a proof principle for the final coalgebra of an endofunctor on a category of data types (resp. domains) is obtained. As an application of the theory developed, an internal full abstraction result for the canonical model of the untyped call-by-value λ-calculus is proved. The operations notion of bisimulation and the denotational notion of final semantics are related by means of conditions under which both coincide

BibTeX

  @InProceedings{Fiore-Acoinductionprincip,
    author = 	 {Marcelo P. Fiore},
    title = 	 {A coinduction principle for recursive data types based on bisimulation },
    booktitle =  {Proceedings of the Eighth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1993},
    year =	 1993,
    editor =	 {Moshe Vardi},
    month =	 {June}, 
    pages =      {110--119},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }