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 | |
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 |
Keywords
- ELEMENTARY AFFINE LOGIC
- ALGORITHM