To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

Fixed Points of Type Cons… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

Fixed Points of Type Constructors and Primitive Recursion

Journal article
Authors Andreas Abel
Ralph Matthes
Published in Lecture Notes in Computer Science
Volume 3210
Pages 190-204
ISSN 0302-9743
Publication year 2004
Published at
Pages 190-204
Language en
Subject categories Computer and Information Science


For nested or heterogeneous datatypes, terminating recursion schemes considered so far have been instances of iteration, excluding efficient definitions of fixed-point unfolding. Two solutions of this problem are proposed: The first one is a system with equi-recursive non-strictly positive type constructors of arbitrary finite kinds, where fixed-point unfolding is computationally invisible due to its treatment on the level of type equality. Positivity is ensured by a polarized kinding system, and strong normalization is proven by a model construction based on saturated sets. The second solution is a formulation of primitive recursion for arbitrary type constructors of any rank. Although without positivity restriction, the second system embeds—even operationally—into the first one.

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?