Skip to main content
Kent Academic Repository

Ensuring Termination in ESFP

Telford, Alastair J., Turner, David A. (2000) Ensuring Termination in ESFP. Journal of Universal Computer Science, 6 (4). pp. 474-488. (doi:10.3217/jucs-006-04) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) (KAR id:21845)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided.
Official URL:
http://www.jucs.org/jucs_6_4/ensuring_termination_...

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: Article
DOI/Identification number: 10.3217/jucs-006-04
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: 16 Oct 2009 15:40 UTC
Last Modified: 05 Nov 2024 10:00 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/21845 (The current URI for this page, for reference purposes)

University of Kent Author Information

Turner, David A..

Creator's ORCID:
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.