School of Computing

Ensuring Streams Flow

Alastair Telford and David Turner

In Michael Johnson, editor, Algebraic Methodology and Software Technology, 6th International Conference, AMAST '97, Sydney Australia, December 1997, volume 1349 of Lecture Notes in Computer Science, pages 182-196. AMAST, Springer-Verlag, December 1997.

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.

Download publication 84 kbytes

Bibtex Record

@inproceedings{499,
author = {Alastair Telford and David Turner},
title = {Ensuring {S}treams {F}low},
month = {December},
year = {1997},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1997/499},
    ISBN = {3-540-63888-1},
    ISSN = {0302-9743},
    booktitle = {Algebraic Methodology and Software Technology, 6th International Conference, AMAST '97, Sydney Australia, December 1997},
    editor = {Michael Johnson},
    organization = {AMAST},
    publisher = {Springer-Verlag},
    refereed = {Yes},
    series = {Lecture Notes in Computer Science},
    volume = {1349},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014