Telford, Alastair J. and Turner, David A. (1997) Ensuring the Productivity of Infinite Structures. Technical report. University of Kent, Canterbury, Kent, CT2 7NF, UK (KAR id:21461)
Other (zip)
Language: English |
|
Download this file (Other/156kB) |
![]() |
Request a format suitable for use with assistive technology e.g. a screenreader | |
PDF
Language: English |
|
Download this file (PDF/465kB) |
Preview |
Request a format suitable for use with assistive technology e.g. a screenreader | |
Postscript
Language: English |
|
Download this file (Postscript/418kB) |
Preview |
Request a format suitable for use with assistive technology e.g. a screenreader |
Abstract
It is our aim to produce an elementary strong functional programming (ESFP) system. To be useful, ESFP should include structures such as streams which can be computationally unwound infinitely often. We describe a syntactic analysis to ensure that infinitely proceeding structures, which we shall term codata , are productive. This analysis is an extension of the check for guardedness that has been used with definitions over coinductive types in Martin-Lof's type theory and in the calculus of constructions. Our analysis is presented as a form of abstract interpretation that allows a wider syntactic class of corecursive definitions to be recognised as productive than in previous work. Thus programmers will have fewer restrictions on their use of infinite streams within a strongly normalizing functional language.
Item Type: | Reports and Papers (Technical report) |
---|---|
Additional information: | This technical report has been revised (March 1998). A shorter version of this paper was presented at AMAST '97. |
Uncontrolled keywords: | Functional programming, codata, productivity, abstract interpretation |
Subjects: | Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
Depositing User: | David Turner |
Date Deposited: | 01 Aug 2009 17:19 UTC |
Last Modified: | 05 Nov 2024 09:59 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/21461 (The current URI for this page, for reference purposes) |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):