Type inference for a polynomial lambda calculus

Marco Gaboardi; Simona Ronchi Della Rocca

doi:10.1007/978-3-642-02444-3_9

Type inference for a polynomial lambda calculus

Marco Gaboardi, Simona Ronchi Della Rocca

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

4 Citations (Scopus)

Abstract

We study the type inference problem for the Soft Type Assignment system (STA) for lambda-calculus introduced in [1], which is correct and complete for polynomial time computations. In particular we design an algorithm which, given in input a A-term, provides all the constraints that need to be satisfied in order to type it. For the propositional fragment of STA, the satisfiability of the constraints is decidable. We conjecture that, for the whole system, the type inference is undecidable, but our algorithm can be used for checking the typability of some particular terms.

Original language	English
Title of host publication	Types for Proofs and Programs
Subtitle of host publication	nternational Conference, TYPES 2008 Torino, Italy, March 26-29, 2008 Revised Selected Papers
Editors	Stefano Berardi, Ferruccio Damiani, Ugo De' Liguoro
Place of Publication	Berlin
Publisher	Springer
Pages	136-152
Number of pages	17
ISBN (Electronic)	9783642024443
ISBN (Print)	9783642024436
DOIs	https://doi.org/10.1007/978-3-642-02444-3_9
Publication status	Published - 2009
Event	Types for Proofs and Programs: International Conference - Villa Gualino, Turin, Italy Duration: 26 Mar 2008 → 29 Mar 2008 http://types2008.di.unito.it/

Publication series

Name	Lecture notes in computer science
Publisher	Springer
Volume	5497
ISSN (Print)	0302-9743

Conference

Conference	Types for Proofs and Programs: International Conference
Abbreviated title	TYPES 2008
Country/Territory	Italy
City	Turin
Period	26/03/08 → 29/03/08
Internet address	http://types2008.di.unito.it/

Keywords

ELEMENTARY AFFINE LOGIC
ALGORITHM

Access to Document

10.1007/978-3-642-02444-3_9

http://library.dundee.ac.uk:80/F/?func=direct&local_base=DUN01&doc_number=000739716

Cite this

Gaboardi, M., & Della Rocca, S. R. (2009). Type inference for a polynomial lambda calculus. In S. Berardi, F. Damiani, & U. De' Liguoro (Eds.), Types for Proofs and Programs: nternational Conference, TYPES 2008 Torino, Italy, March 26-29, 2008 Revised Selected Papers (pp. 136-152). (Lecture notes in computer science; Vol. 5497). Springer . https://doi.org/10.1007/978-3-642-02444-3_9

@inproceedings{6e23180a217c4cc39de02e30c4ab8642,

title = "Type inference for a polynomial lambda calculus",

abstract = "We study the type inference problem for the Soft Type Assignment system (STA) for lambda-calculus introduced in [1], which is correct and complete for polynomial time computations. In particular we design an algorithm which, given in input a A-term, provides all the constraints that need to be satisfied in order to type it. For the propositional fragment of STA, the satisfiability of the constraints is decidable. We conjecture that, for the whole system, the type inference is undecidable, but our algorithm can be used for checking the typability of some particular terms.",

keywords = "ELEMENTARY AFFINE LOGIC, ALGORITHM",

author = "Marco Gaboardi and {Della Rocca}, {Simona Ronchi}",

year = "2009",

doi = "10.1007/978-3-642-02444-3_9",

language = "English",

isbn = "9783642024436",

series = "Lecture notes in computer science",

publisher = "Springer ",

pages = "136--152",

editor = "Stefano Berardi and Ferruccio Damiani and {De' Liguoro}, Ugo",

booktitle = "Types for Proofs and Programs",

note = "Types for Proofs and Programs: International Conference, TYPES 2008 ; Conference date: 26-03-2008 Through 29-03-2008",

url = "http://types2008.di.unito.it/",

}

Gaboardi, M & Della Rocca, SR 2009, Type inference for a polynomial lambda calculus. in S Berardi, F Damiani & U De' Liguoro (eds), Types for Proofs and Programs: nternational Conference, TYPES 2008 Torino, Italy, March 26-29, 2008 Revised Selected Papers. Lecture notes in computer science, vol. 5497, Springer , Berlin, pp. 136-152, Types for Proofs and Programs: International Conference, Turin, Italy, 26/03/08. https://doi.org/10.1007/978-3-642-02444-3_9

Type inference for a polynomial lambda calculus. / Gaboardi, Marco; Della Rocca, Simona Ronchi.
Types for Proofs and Programs: nternational Conference, TYPES 2008 Torino, Italy, March 26-29, 2008 Revised Selected Papers. ed. / Stefano Berardi; Ferruccio Damiani; Ugo De' Liguoro. Berlin: Springer , 2009. p. 136-152 (Lecture notes in computer science; Vol. 5497).

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

TY - GEN

T1 - Type inference for a polynomial lambda calculus

AU - Gaboardi, Marco

AU - Della Rocca, Simona Ronchi

PY - 2009

Y1 - 2009

N2 - We study the type inference problem for the Soft Type Assignment system (STA) for lambda-calculus introduced in [1], which is correct and complete for polynomial time computations. In particular we design an algorithm which, given in input a A-term, provides all the constraints that need to be satisfied in order to type it. For the propositional fragment of STA, the satisfiability of the constraints is decidable. We conjecture that, for the whole system, the type inference is undecidable, but our algorithm can be used for checking the typability of some particular terms.

AB - We study the type inference problem for the Soft Type Assignment system (STA) for lambda-calculus introduced in [1], which is correct and complete for polynomial time computations. In particular we design an algorithm which, given in input a A-term, provides all the constraints that need to be satisfied in order to type it. For the propositional fragment of STA, the satisfiability of the constraints is decidable. We conjecture that, for the whole system, the type inference is undecidable, but our algorithm can be used for checking the typability of some particular terms.

KW - ELEMENTARY AFFINE LOGIC

KW - ALGORITHM

U2 - 10.1007/978-3-642-02444-3_9

DO - 10.1007/978-3-642-02444-3_9

M3 - Conference contribution

SN - 9783642024436

T3 - Lecture notes in computer science

SP - 136

EP - 152

BT - Types for Proofs and Programs

A2 - Berardi, Stefano

A2 - Damiani, Ferruccio

A2 - De' Liguoro, Ugo

PB - Springer

CY - Berlin

T2 - Types for Proofs and Programs: International Conference

Y2 - 26 March 2008 through 29 March 2008

ER -

Type inference for a polynomial lambda calculus

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this