Coinductive axiomatization of recursive type equality and subtyping

[Brian T. Rice]

At 03:10 PM 1/29/00 +0100, Massimo Dentico wrote:
>I hope that this paper is useful to the Slate project.
>
>http://www.diku.dk/research-groups/topps/bibliography/1997.html#D-322
>==================================================================
>D-322.   
>
>M Brandt and F Henglein.
>
>Coinductive  axiomatization  of  recursive type  equality and sub-
>typing.
>
>In Proc. 3d Int'l Conf.  on  Typed Lambda Calculi and Applications
>(TLCA), Nancy, France, April 2-4, 1997 ( R Hindley, ed.),  pp. 63-
>81. Volume 1210 of Lecture Notes in Computer Science (LNCS).
>Springer-Verlag. April, 1997.
>
>Keywords: Recursive types, type equality, subtyping,
>axiomatization, coinduction 
>
>Summary: We present new sound and complete axiomatizations of type
>equality  and  subtype inequality  for a first-order type language
>with  regular  recursive   types.   The  rules  are  motivated  by
>coinductive  characterizations   of  type  containment   and  type
>equality via simulation and bisimulation,  respectively.  The main
>novelty of the axiomatization is the fixpoint rule (or coinduction
>principle).   The  new axiomatizations  give  rise  to  a  natural
>operational interpretation of proofs as coercions and to efficient
>algorithms  for constructing explicit  coercions efficiently,  not
>only deciding type equality and type containment.
>==================================================================
>
>Postscript: ftp://ftp.diku.dk/diku/semantics/papers/D-322.ps.gz
>
>-- 
>Massimo Dentico

Yes, quite useful, thank you. However, the coinductive typing is far from
being realizable in the spec, so don't hold your breath just yet waiting
for implementation of the ideas. :)

Actually, most likely there will be a tiny kernel of support for
co-inductive ideas in the language, with the primary support for these
ideas coming from Mobius (which of course would require a working
implementation).

I'll be writing soon about co-induction and Slate soon.

	Brian