A Coinduction Principle for Recursive Data Types
                     Based on Bisimulation

                       Marcelo P. Fiore

                Department of Computer Science 
         Laboratory for Foundations of Computer Science 
         University of Edinburgh, The King's Buildings 
                 Edinburgh EH9 3JZ, Scotland 
 
                      <mf@dcs.ed.ac.uk>
 
                           Synopsis

The concept of bisimulation from concurrency 
theory~\cite{Park81,Milner89} 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 (in the sense of~\cite{AbramskyOng92}) for the canonical model 
of the untyped call-by-value $\lambda$-calculus is proved.

Also, the operational notion of bisimulation and the denotational 
notion of final semantics are related by means of conditions under 
which both coincide.