article · 2014

Under consideration for publication in J. Functional Programming 1 Wellfounded Recursion with Copatterns and Sized Types

Andreas Abel, Brigitte Pientka

Cited by 0Abstract and details only

Abstract

In this paper, we study strong normalization of a core language based on System Fω 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ω 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. 1

Cite this paper

APA 7

Abel, A., & Pientka, B. (2014). Under consideration for publication in J. Functional Programming 1 Wellfounded Recursion with Copatterns and Sized Types.

MLA 9

Abel, Andreas, and Brigitte Pientka. “Under consideration for publication in J. Functional Programming 1 Wellfounded Recursion with Copatterns and Sized Types.” 2014.

Chicago

Abel, Andreas, and Brigitte Pientka. 2014. “Under consideration for publication in J. Functional Programming 1 Wellfounded Recursion with Copatterns and Sized Types.”

Harvard

Abel, A. and Pientka, B. (2014) ‘Under consideration for publication in J. Functional Programming 1 Wellfounded Recursion with Copatterns and Sized Types’.

BibTeX

@article{abel2014under,
  title = {{Under consideration for publication in J. Functional Programming 1 Wellfounded Recursion with Copatterns and Sized Types}},
  author = {Abel, Andreas and Pientka, Brigitte},
  year = {2014}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.