To the top

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

Tell a friend about this page
Print version

Well-founded recursion wi… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

Well-founded recursion with copatterns and sized types

Journal article
Authors Andreas Abel
B. Pientka
Published in Journal of Functional Programming
Volume 26
ISSN 0956-7968
Publication year 2016
Published at Department of Computer Science and Engineering (GU)
Language en
Keywords rewrite systems, termination, definitions, productivity, calculus, Computer Science
Subject categories Computer and Information Science


In this paper, we study strong normalization of a core language based on System F-omega which supports programming with finite and infinite structures. Finite data such as finite lists and trees is defined via constructors and manipulated via pattern matching, while infinite data such as streams and infinite trees is defined by observations and synthesized via copattern matching. Taking a type-based approach to strong normalization, we track size information about finite and infinite data in the type. We exploit the duality of pattern and copatterns to give a unifying semantic framework which allows us to elegantly and uniformly support both well-founded induction and coinduction by rewriting. The strong normalization proof is structured around Girard's reducibility candidates. As such, our system allows for non determinism and does not rely on coverage. Since System F-omega is general enough that it can be the target of compilation for the Calculus of Constructions, this work is a significant step towards representing observation-based infinite data in proof assistants such as Coq and Agda.

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?