[Prev][Next][Index][Thread]
Results about F^omega with type fixed-points ?!
-
To: types@cis.upenn.edu
-
Subject: Results about F^omega with type fixed-points ?!
-
From: Andreas Abel <abel@informatik.uni-muenchen.de>
-
Date: Tue, 23 Sep 2003 19:53:41 +0200
-
Organization: LMU Muenchen
-
User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.3) Gecko/20030312
Currently I am studying extensions of System F^omega by positive
fixed-points of type operators. These fixed-points are useful to
formalize so-called heterogeneous or nested datatypes. An example of
such a fixed-point would be
PList : * -> *
PList = \A. A + PList (A x A)
which denotes powerlists resp. perfectly balanced leaf-labelled trees.
My question: Is something known about extensions of F^omega by
higher-order fixed-points like "PList"? Does a proof of normalization
exist?
The literature I came across only deals with positive fixed-points of
kind "*" (lists, trees ...) or with fixed-points that are not positive
and hence destroy normalization.
Any hints very much appreciated.
Cheers,
Andreas
--
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/