A soft type assignment system for λ-calculus

Marco Gaboardi, Simona Ronchi Della Rocca

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    26 Citations (Scopus)

    Abstract

    Soft Linear Logic (SLL) is a subsystem of second-order linear logic with restricted rules for exponentials, which is correct and complete for PTIME. We design a type assignment system for the ?-calculus (STA), which assigns to ?-terms as types (a proper subset of) SLL formulas, in such a way that typable terms inherit the good complexity properties of the logical system. Namely STA enjoys subject reduction and normalization, and it is correct and complete for PTIME and PTIME.

    Original languageEnglish
    Title of host publicationComputer Science Logic
    Subtitle of host publication21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007. Proceedings
    EditorsJacques Duparc, Thomas A. Henzinger
    Place of PublicationBerlin
    PublisherSpringer
    Pages253-267
    Number of pages15
    ISBN (Electronic)9783540749158
    ISBN (Print)9783540749141
    DOIs
    Publication statusPublished - 2007
    Event21st International Workshop on Computer Science Logic, CSL 2007/16th Annual Conference of the EACSL - Lausanne, Switzerland
    Duration: 11 Sep 200715 Sep 2007

    Publication series

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

    Conference

    Conference21st International Workshop on Computer Science Logic, CSL 2007/16th Annual Conference of the EACSL
    Country/TerritorySwitzerland
    CityLausanne
    Period11/09/0715/09/07

    Keywords

    • LAMBDA-CALCULUS
    • POLYNOMIAL-TIME
    • LINEAR LOGIC

    Cite this