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

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

doi:10.1007/978-3-540-74464-1_15

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

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	Types for Proofs and Programs: International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers
Editors	T. Altenkirch, C. McBride
Publisher	Springer
Pages	221-236
Number of pages	16
ISBN (Print)	978-3-540-74463-4
DOIs	https://doi.org/10.1007/978-3-540-74464-1_15
Publication status	Published - 2007
Event	International Workshop, TYPES 2006 - Nottingham, United Kingdom Duration: 18 Apr 2006 → 21 Apr 2006

Publication series

Name	Lecture Notes in Computer Science
Volume	4502
ISSN (Print)	0302-9743

Conference

Conference	International Workshop, TYPES 2006
Country/Territory	United Kingdom
City	Nottingham
Period	18/04/06 → 21/04/06

Keywords

RANK-2 INTERSECTION

Access to Document

10.1007/978-3-540-74464-1_15

EP/C001346/1: Generative Programming for Embedded Systems
Hammond, K. (PI)
EPSRC
1/01/05 → 31/12/07
Project: Standard

Cite this

Simoes, H. R., Hammond, K., Florido, M., & Vasconcelos, P. (2007). Using intersection types for cost-analysis of higher-order polymorphic functional programs. In T. Altenkirch, & C. McBride (Eds.), Types for Proofs and Programs: International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers (pp. 221-236). (Lecture Notes in Computer Science; Vol. 4502). Springer. https://doi.org/10.1007/978-3-540-74464-1_15

Simoes, Hugo R. ; Hammond, Kevin ; Florido, Mario et al. / Using intersection types for cost-analysis of higher-order polymorphic functional programs. Types for Proofs and Programs: International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers. editor / T. Altenkirch ; C. McBride. Springer, 2007. pp. 221-236 (Lecture Notes in Computer Science).

@inproceedings{ca0c1d2eeea7429fb051f055c4ea4dc7,

title = "Using intersection types for cost-analysis of higher-order polymorphic functional programs",

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.",

keywords = "RANK-2 INTERSECTION",

author = "Simoes, {Hugo R.} and Kevin Hammond and Mario Florido and Pedro Vasconcelos",

year = "2007",

doi = "10.1007/978-3-540-74464-1_15",

language = "English",

isbn = "978-3-540-74463-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "221--236",

editor = "T. Altenkirch and C. McBride",

booktitle = "Types for Proofs and Programs: International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers",

address = "Netherlands",

note = "International Workshop, TYPES 2006 ; Conference date: 18-04-2006 Through 21-04-2006",

}

Simoes, HR, Hammond, K, Florido, M & Vasconcelos, P 2007, Using intersection types for cost-analysis of higher-order polymorphic functional programs. in T Altenkirch & C McBride (eds), Types for Proofs and Programs: International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers. Lecture Notes in Computer Science, vol. 4502, Springer, pp. 221-236, International Workshop, TYPES 2006, Nottingham, United Kingdom, 18/04/06. https://doi.org/10.1007/978-3-540-74464-1_15

Using intersection types for cost-analysis of higher-order polymorphic functional programs. / Simoes, Hugo R.; Hammond, Kevin; Florido, Mario et al.
Types for Proofs and Programs: International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers. ed. / T. Altenkirch; C. McBride. Springer, 2007. p. 221-236 (Lecture Notes in Computer Science; Vol. 4502).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

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

AU - Simoes, Hugo R.

AU - Hammond, Kevin

AU - Florido, Mario

AU - Vasconcelos, Pedro

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

KW - RANK-2 INTERSECTION

U2 - 10.1007/978-3-540-74464-1_15

DO - 10.1007/978-3-540-74464-1_15

M3 - Conference contribution

SN - 978-3-540-74463-4

T3 - Lecture Notes in Computer Science

SP - 221

EP - 236

BT - Types for Proofs and Programs: International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers

A2 - Altenkirch, T.

A2 - McBride, C.

PB - Springer

T2 - International Workshop, TYPES 2006

Y2 - 18 April 2006 through 21 April 2006

ER -

Simoes HR, Hammond K, Florido M, Vasconcelos P. Using intersection types for cost-analysis of higher-order polymorphic functional programs. In Altenkirch T, McBride C, editors, Types for Proofs and Programs: International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers. Springer. 2007. p. 221-236. (Lecture Notes in Computer Science). doi: 10.1007/978-3-540-74464-1_15

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

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Projects

EP/C001346/1: Generative Programming for Embedded Systems

Cite this