Please use this identifier to cite or link to this item: http://hdl.handle.net/2381/28332
Title: Pure Type Systems with Corecursion on Streams: From Finite to Infinitary Normalisation
Authors: Severi, Paula
de Vries, Fer-Jan
First Published: 12-Sep-2012
Presented at: The 17th ACM SIGPLAN International Conference on Functional Programming (ICFP 2012), Copenhagen, Denmark
Start Date: 10-Sep-2012
End Date: 12-Sep-2012
Publisher: Association for Computing Machinery (ACM)
Citation: Severi, 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
Abstract: 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.
DOI Link: 10.1145/2398856.2364550
ISBN: 978-1-4503-1054-3
Links: http://dl.acm.org/citation.cfm?doid=2364527.2364550
http://icfpconference.org/icfp2012/
http://hdl.handle.net/2381/28332
Version: Post-print
Status: Peer-reviewed
Type: Conference Paper
Rights: Copyright © ACM, 2012. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proceedings of the 17th ACM SIGPLAN international conference on Functional programming (2012), http://doi.acm.org/10.1145/2364527.2364550.
Appears in Collections:Conference Papers & Presentations, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
mainICFP2012.pdfPost-review (final submitted)324.16 kBAdobe PDFView/Open


Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.