Wellfounded recursion with copatterns: a unified approach to termination and productivity

• In this paper, we study strong normalization of a core language basedon System F-omega which supports programming with finite and infinitestructures. Building on our prior work, finite data such as finitelists and trees are defined via constructors and manipulated viapattern matching, while infinite data such as streams and infinitetrees is defined by observations and synthesized via copatternmatching. In this work, we take a type-based approach to strongnormalization by tracking size information about finite and infinitedata in the type. This guarantees compositionality. More importantly,the duality of pattern and copatterns provide a unifying semanticconcept which allows us for the first time to elegantly and uniformlysupport both well-founded induction and coinduction by mererewriting.The strong normalization proof is structured around Girard'sreducibility candidates. As such our system allows for non-determinismand does not rely on coverage. Since System F-omega is general enoughthat it can be the target of compilation for the Calculus ofConstructions, this work is a significant step towards representingobservation-centric infinite data in proof assistants such as Coq and Agda.

Subject headings

NATURVETENSKAP  -- Data- och informationsvetenskap (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences (hsv//eng)

NATURVETENSKAP  -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences -- Computer Sciences (hsv//eng)

Publication and Content Type

kon (subject category)

ref (subject category)