Telford, Alastair J. and Turner, David A. (2000) A Hierarchy of Languages with Strong Termination Properties. Technical report. University of Kent, The Computing Laboratory, The University, Canterbury, Kent, CT2 7NF (KAR id:22050)
Other (zd)
Language: English |
|
Download this file (Other/755kB) |
![]() |
Request a format suitable for use with assistive technology e.g. a screenreader | |
PDF
Language: English |
|
Download this file (PDF/709kB) |
Preview |
Request a format suitable for use with assistive technology e.g. a screenreader |
Abstract
In previous papers we have proposed an elementary discipline of strong functional programming (ESFP), in which all computations terminate. A key feature of the discipline is that we introduce a type distinction between data which is known to be finite, and codata which is (potentially) infinite. To ensure termination, recursion over data must be well-founded, and corecursion (the definition schema for codata) must be productive, and both of these restrictions must be enforced automatically by the compiler. In our previous work we used abstract interpretation to establish the productivity of corecursive definitions in an elementary strong functional language. We show here that similar ideas can be applied in the dual case to check whether recursive function definitions are strongly normalising. We thus exhibit a powerful termination analysis technique which we demonstrate can be extended to partial functions.
Item Type: | Reports and Papers (Technical report) |
---|---|
Additional information: | Paper currently under revision |
Uncontrolled keywords: | Termination analysis, Abstract interpretation, Elementary Strong Functional Programming |
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: | 30 Aug 2009 17:44 UTC |
Last Modified: | 16 Nov 2021 10:00 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/22050 (The current URI for this page, for reference purposes) |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):