[Prev][Next][Index][Thread]
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:
http://protis.univ-mrs.fr/~amadio/biblio_my_amadio.html
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
ABSTRACT
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.
---------------