mainICFP2012.pdf (324.16 kB)
Pure Type Systems with Corecursion on Streams: From Finite to Infinitary Normalisation
conference contributionposted on 2013-10-28, 15:24 authored by Paula Severi, Fer-Jan de Vries
In this paper, we use types for ensuring that programs involving streams are well-behaved.We extend pure type systems with a type constructor for streams, a modal operator next and a fixed point operator for expressing corecursion. This extension is called Pure Type Systems with Corecursion (CoPTS). The typed lambda calculus for reactive programs defined by Krishnaswami and Benton can be obtained as a CoPTS. CoPTSs allow us to study a wide range of typed lambda calculi extended with corecursion using only one framework. In particular, we study this extension for the calculus of constructions which is the underlying formal language of Coq. We use the machinery of infinitary rewriting and formalise the idea of well-behaved programs using the concept of infinitary normalisation. The set of finite and infinite terms is defined as a metric completion. We establish a precise connection between the modal operator (• A) and the metric at a syntactic level by relating a variable of type (• A) with the depth of all its occurrences in a term. This syntactic connection between the modal operator and the depth is the key to the proofs of infinitary weak and strong normalisation.
CitationSeveri, P.; de Vries, F. ‘Pure Type Systems with Corecursion on Streams: From Finite to Infinitary Normalisation’ in ICFP '12 - Proceedings of the 17th ACM SIGPLAN international conference on Functional programming (© 2012 AMC), pp. 141-152
Author affiliation/Organisation/COLLEGE OF SCIENCE AND ENGINEERING/Department of Computer Science
SourceThe 17th ACM SIGPLAN International Conference on Functional Programming (ICFP 2012), Copenhagen, Denmark
- AM (Accepted Manuscript)