A coinduction principle for recursive data types based on bisimulation
- 31 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 110-119
- https://doi.org/10.1109/lics.1993.287595
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 lambda -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
This publication has 11 references indexed in Scilit:
- Concurrency and automata on infinite sequencesPublished by Springer Nature ,2005
- A final coalgebra theoremPublished by Springer Nature ,2005
- Recursive types reduced to inductive typesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A co-induction principle for recursively defined domainsTheoretical Computer Science, 1994
- Partiality, cartesian closedness, and toposesInformation and Computation, 1989
- Fundamental properties of infinite treesTheoretical Computer Science, 1983
- The Category-Theoretic Solution of Recursive Domain EquationsSIAM Journal on Computing, 1982
- Parametrized data types do not need highly constrained parametersInformation and Control, 1982
- The denotational semantics of sequential machinesInformation Processing Letters, 1980
- On the semantics of fair parallelismPublished by Springer Nature ,1980