[Prev][Next][Index][Thread]
Results about F^omega with type fixedpoints ?!

To: types@cis.upenn.edu

Subject: Results about F^omega with type fixedpoints ?!

From: Andreas Abel <abel@informatik.unimuenchen.de>

Date: Tue, 23 Sep 2003 19:53:41 +0200

Organization: LMU Muenchen

UserAgent: Mozilla/5.0 (X11; U; Linux i686; enUS; rv:1.3) Gecko/20030312
Currently I am studying extensions of System F^omega by positive
fixedpoints of type operators. These fixedpoints are useful to
formalize socalled heterogeneous or nested datatypes. An example of
such a fixedpoint would be
PList : * > *
PList = \A. A + PList (A x A)
which denotes powerlists resp. perfectly balanced leaflabelled trees.
My question: Is something known about extensions of F^omega by
higherorder fixedpoints like "PList"? Does a proof of normalization
exist?
The literature I came across only deals with positive fixedpoints of
kind "*" (lists, trees ...) or with fixedpoints 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.unimuenchen.de/~abel/