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


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

School/Research organisations


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.



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
Number of pages16
ISBN (Print)978-3-540-74463-4
StatePublished - 2007
EventInternational Workshop, TYPES 2006 - Nottingham, United Kingdom
Duration: 18 Apr 200621 Apr 2006

Publication series

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


ConferenceInternational Workshop, TYPES 2006
CountryUnited Kingdom

    Research areas


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