Type inference for a polynomial lambda calculus

Marco Gaboardi, Simona Ronchi Della Rocca

    Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish
    Title of host publicationTypes for Proofs and Programs
    Subtitle of host publicationnternational Conference, TYPES 2008 Torino, Italy, March 26-29, 2008 Revised Selected Papers
    EditorsStefano Berardi, Ferruccio Damiani, Ugo De' Liguoro
    Place of PublicationBerlin
    PublisherSpringer
    Pages136-152
    Number of pages17
    ISBN (Electronic)9783642024443
    ISBN (Print)9783642024436
    DOIs
    Publication statusPublished - 2009
    EventTypes for Proofs and Programs: International Conference - Villa Gualino, Turin, Italy
    Duration: 26 Mar 200829 Mar 2008
    http://types2008.di.unito.it/

    Publication series

    NameLecture notes in computer science
    PublisherSpringer
    Volume5497
    ISSN (Print)0302-9743

    Conference

    ConferenceTypes for Proofs and Programs: International Conference
    Abbreviated titleTYPES 2008
    Country/TerritoryItaly
    CityTurin
    Period26/03/0829/03/08
    Internet address

    Keywords

    • ELEMENTARY AFFINE LOGIC
    • ALGORITHM

    Fingerprint

    Dive into the research topics of 'Type inference for a polynomial lambda calculus'. Together they form a unique fingerprint.

    Cite this