Paper on co-inductive Types

I would like to announce the following paper on co-inductive types
which is appeared as `Rapport 245 of Laboratoire d'Informatique de
Marseille' and is available at the following address:


Of course, comments are welcome. 

Roberto Amadio


	Analysis of a guard condition in type theory
		(preliminary report)

	Roberto M. Amadio and Solange Coupet-Grimal
	    Universite' de Provence, Marseille


We present a realizability interpretation of co-inductive types based
on partial equivalence relations (per's).  We extract from the per's
interpretation sound rules to type recursive definitions.  These
recursive definitions are needed to introduce ``infinite'' and
``total'' objects of co-inductive type such as an infinite stream or a
non-terminating process.  We show that the proposed type system enjoys
the basic syntactic properties of subject reduction and strong
normalization with respect to a confluent rewriting system first
studied by Gimenez.  We also compare the proposed type system with
those studied by Coquand and Gimenez. In particular, we provide a
semantic reconstruction of Gimenez's system which suggests a rule to
type nested recursive definitions.