Skip to content

Research at St Andrews

Using intersection types for cost-analysis of higher-order polymorphic functional programs

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Author(s)

Hugo R. Simoes, Kevin Hammond, Mario Florido, Pedro Vasconcelos

School/Research organisations

Abstract

This paper presents a system of cost derivation for higher-order and polymorphic functional programs based on a notion of sized types and exploiting a type-and-effect system approach. The paper gives an operational semantics of cost for a simple strict functional language in terms of lambda-calculus beta-reduction steps and introduces type rules describing cost effects. The type system is based on intersection types. The use of discrete polymorphism (intersection types) instead of the usual parametric polymorphism approach improves the analysis and solves, in many cases, the "size aliasing problem" that has been identified as " limitation on previous type-and-effect approaches. Finally we provide " proof of the soundness of our effect system with respect to the cost semantics.

Close

Details

Original languageEnglish
Title of host publicationTypes for Proofs and Programs: International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers
EditorsT. Altenkirch, C. McBride
PublisherSpringer
Pages221-236
Number of pages16
ISBN (Print)978-3-540-74463-4
DOIs
StatePublished - 2007
EventInternational Workshop, TYPES 2006 - Nottingham, United Kingdom
Duration: 18 Apr 200621 Apr 2006

Publication series

NameLecture Notes in Computer Science
Volume4502
ISSN (Print)0302-9743

Conference

ConferenceInternational Workshop, TYPES 2006
CountryUnited Kingdom
CityNottingham
Period18/04/0621/04/06

    Research areas

  • RANK-2 INTERSECTION

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Automatically deriving cost models for structured parallel processes using hylomorphisms

    Castro, D., Hammond, K., Sarkar, S. & Alguwaifli, Y. Feb 2018 In : Future Generation Computer Systems. 79, Part 2, p. 653-668

    Research output: Contribution to journalArticle

  2. The Missing Link! A new skeleton for evolutionary multi-agent systems in Erlang

    Stypka, J., Turek, W., Byrski, A., Kisiel-Dorohinicki, M., Barwell, A. D., Brown, C. M., Hammond, K. & Janjic, V. Feb 2018 In : International Journal of Parallel Programming. 46, 1, p. 4-22 19 p.

    Research output: Contribution to journalArticle

  3. Proof-relevant Horn clauses for dependent type inference and term synthesis

    Farka, F., Komendantskya, E. & Hammond, K. 2018 In : Theory and Practice of Logic Programming. 18, 3-4, p. 484-501

    Research output: Contribution to journalArticle

  4. Type-based cost analysis for lazy functional languages

    Jost, S., Vasconcelos, P., Florido, M. & Hammond, K. Jun 2017 In : Journal of Automated Reasoning. 59, 1, p. 87-120 34 p.

    Research output: Contribution to journalArticle

ID: 6640770