From light logics to type assignments

a case study

Marco Gaboardi, Simona Ronchi Della Rocca

    Research output: Contribution to journalArticle

    1 Citation (Scopus)

    Abstract

    Using Soft Linear Logic (SLL) as case study, we analyze a method for transforming a light logic into a type assignment system for the ?-calculus, inheriting the complexity properties of the logics. Namely the typing assures the strong normalization in a number of steps polynomial in the size of the term, and moreover all polynomial functions can be computed by ?-terms that can be typed in the system. The proposed method is general enough to be used also for other light logics.
    Original languageEnglish
    Pages (from-to)499-530
    Number of pages32
    JournalLogic Journal of the IGPL
    Volume17
    Issue number5
    DOIs
    Publication statusPublished - Oct 2009

    Fingerprint

    Assignment
    Logic
    Linear Logic
    Normalization
    Calculi

    Cite this

    Gaboardi, Marco ; Rocca, Simona Ronchi Della. / From light logics to type assignments : a case study. In: Logic Journal of the IGPL. 2009 ; Vol. 17, No. 5. pp. 499-530.
    @article{479cf8682d9640589b11d6b334c000f1,
    title = "From light logics to type assignments: a case study",
    abstract = "Using Soft Linear Logic (SLL) as case study, we analyze a method for transforming a light logic into a type assignment system for the ?-calculus, inheriting the complexity properties of the logics. Namely the typing assures the strong normalization in a number of steps polynomial in the size of the term, and moreover all polynomial functions can be computed by ?-terms that can be typed in the system. The proposed method is general enough to be used also for other light logics.",
    author = "Marco Gaboardi and Rocca, {Simona Ronchi Della}",
    year = "2009",
    month = "10",
    doi = "10.1093/jigpal/jzp019",
    language = "English",
    volume = "17",
    pages = "499--530",
    journal = "Logic Journal of the IGPL",
    issn = "1367-0751",
    publisher = "Oxford University Press",
    number = "5",

    }

    From light logics to type assignments : a case study. / Gaboardi, Marco; Rocca, Simona Ronchi Della.

    In: Logic Journal of the IGPL, Vol. 17, No. 5, 10.2009, p. 499-530.

    Research output: Contribution to journalArticle

    TY - JOUR

    T1 - From light logics to type assignments

    T2 - a case study

    AU - Gaboardi, Marco

    AU - Rocca, Simona Ronchi Della

    PY - 2009/10

    Y1 - 2009/10

    N2 - Using Soft Linear Logic (SLL) as case study, we analyze a method for transforming a light logic into a type assignment system for the ?-calculus, inheriting the complexity properties of the logics. Namely the typing assures the strong normalization in a number of steps polynomial in the size of the term, and moreover all polynomial functions can be computed by ?-terms that can be typed in the system. The proposed method is general enough to be used also for other light logics.

    AB - Using Soft Linear Logic (SLL) as case study, we analyze a method for transforming a light logic into a type assignment system for the ?-calculus, inheriting the complexity properties of the logics. Namely the typing assures the strong normalization in a number of steps polynomial in the size of the term, and moreover all polynomial functions can be computed by ?-terms that can be typed in the system. The proposed method is general enough to be used also for other light logics.

    U2 - 10.1093/jigpal/jzp019

    DO - 10.1093/jigpal/jzp019

    M3 - Article

    VL - 17

    SP - 499

    EP - 530

    JO - Logic Journal of the IGPL

    JF - Logic Journal of the IGPL

    SN - 1367-0751

    IS - 5

    ER -