Lics

ACM/IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Eighth Annual IEEE Symposium on

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 Symposium on Logic in Computer Science (LICS 1993)},
    year =	 {1993},
    month =	 {June}, 
    pages =      {110--119},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2022-10-3113:49
Sam Staton