Title :
A coinduction principle for recursive data types based on bisimulation
Author :
Fiore, Marcelo P.
Author_Institution :
Dept. of Comput. Sci., Edinburgh Univ., UK
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
Keywords :
data structures; lambda calculus; parallel algorithms; recursive functions; bisimulation; canonical model; coinduction principle; concurrency theory; denotational notion; endofunctor; equality relation; final coalgebra; internal full abstraction result; proof principle; recursive data types; recursively defined data types; strong-extensionality theorems; untyped call-by-value lambda calculus; Application software; Computer science; Concurrent computing; Councils; Laboratories; Network address translation; Tail;
Conference_Titel :
Logic in Computer Science, 1993. LICS '93., Proceedings of Eighth Annual IEEE Symposium on
Conference_Location :
Montreal, Que.
Print_ISBN :
0-8186-3140-6
DOI :
10.1109/LICS.1993.287595
