From light logics to type assignments:  a case study

Marco Gaboardi; Simona Ronchi Della Rocca

doi:10.1093/jigpal/jzp019

From light logics to type assignments: a case study

Marco Gaboardi, Simona Ronchi Della Rocca

Research output: Contribution to journal › Article › peer-review

3 Citations (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 language	English
Pages (from-to)	499-530
Number of pages	32
Journal	Logic Journal of the Interest Group in Pure and Applied Logic (IGPL) (Logic Journal of the IGPL)
Volume	17
Issue number	5
DOIs	https://doi.org/10.1093/jigpal/jzp019
Publication status	Published - Oct 2009

Access to Document

10.1093/jigpal/jzp019

Cite this

@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 = oct,

doi = "10.1093/jigpal/jzp019",

language = "English",

volume = "17",

pages = "499--530",

journal = "Logic Journal of the Interest Group in Pure and Applied Logic (IGPL) (Logic Journal of the IGPL)",

issn = "1367-0751",

publisher = "Oxford University Press",

number = "5",

}

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

SN - 1367-0751

VL - 17

SP - 499

EP - 530

JO - Logic Journal of the Interest Group in Pure and Applied Logic (IGPL) (Logic Journal of the IGPL)

JF - Logic Journal of the Interest Group in Pure and Applied Logic (IGPL) (Logic Journal of the IGPL)

IS - 5

ER -

From light logics to type assignments: a case study

Abstract

Access to Document

Fingerprint

Cite this