Coinductive axiomatization of recursive type equality and subtyping

[Massimo Dentico]

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