A soft type assignment system for λ-calculus

Marco Gaboardi; Simona Ronchi Della Rocca

doi:10.1007/978-3-540-74915-8_21

A soft type assignment system for λ-calculus

Marco Gaboardi, Simona Ronchi Della Rocca

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

32 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 language	English
Title of host publication	Computer Science Logic
Subtitle of host publication	21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007. Proceedings
Editors	Jacques Duparc, Thomas A. Henzinger
Place of Publication	Berlin
Publisher	Springer
Pages	253-267
Number of pages	15
ISBN (Electronic)	9783540749158
ISBN (Print)	9783540749141
DOIs	https://doi.org/10.1007/978-3-540-74915-8_21
Publication status	Published - 2007
Event	21st International Workshop on Computer Science Logic, CSL 2007/16th Annual Conference of the EACSL - Lausanne, Switzerland Duration: 11 Sept 2007 → 15 Sept 2007

Publication series

Name	Lecture notes in computer science
Publisher	Springer
Volume	4646
ISSN (Print)	0302-9743

Conference

Conference	21st International Workshop on Computer Science Logic, CSL 2007/16th Annual Conference of the EACSL
Country/Territory	Switzerland
City	Lausanne
Period	11/09/07 → 15/09/07

Keywords

LAMBDA-CALCULUS
POLYNOMIAL-TIME
LINEAR LOGIC

Access to Document

10.1007/978-3-540-74915-8_21

http://library.dundee.ac.uk/F/DKB2MQBCCJBR85C2DRQXSCHE97RI8RS35K4F3TV9KLC2M67E5T-22065?func=find-e&adjacent=N&request=9783540749158&find_scan_code=FIND_WRD&x=51&y=9

Cite this

Gaboardi, M., & Della Rocca, S. R. (2007). A soft type assignment system for λ-calculus. In J. Duparc, & T. A. Henzinger (Eds.), Computer Science Logic: 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007. Proceedings (pp. 253-267). (Lecture notes in computer science; Vol. 4646). Springer . https://doi.org/10.1007/978-3-540-74915-8_21

Gaboardi, Marco ; Della Rocca, Simona Ronchi. / A soft type assignment system for λ-calculus. Computer Science Logic: 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007. Proceedings. editor / Jacques Duparc ; Thomas A. Henzinger. Berlin : Springer , 2007. pp. 253-267 (Lecture notes in computer science).

@inproceedings{1fe37464ba2a43179a879f1e07c069df,

title = "A soft type assignment system for λ-calculus",

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.",

keywords = "LAMBDA-CALCULUS, POLYNOMIAL-TIME, LINEAR LOGIC",

author = "Marco Gaboardi and {Della Rocca}, {Simona Ronchi}",

year = "2007",

doi = "10.1007/978-3-540-74915-8_21",

language = "English",

isbn = "9783540749141",

series = "Lecture notes in computer science",

publisher = "Springer ",

pages = "253--267",

editor = "Jacques Duparc and Henzinger, {Thomas A.}",

booktitle = "Computer Science Logic",

note = "21st International Workshop on Computer Science Logic, CSL 2007/16th Annual Conference of the EACSL ; Conference date: 11-09-2007 Through 15-09-2007",

}

Gaboardi, M & Della Rocca, SR 2007, A soft type assignment system for λ-calculus. in J Duparc & TA Henzinger (eds), Computer Science Logic: 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007. Proceedings. Lecture notes in computer science, vol. 4646, Springer , Berlin, pp. 253-267, 21st International Workshop on Computer Science Logic, CSL 2007/16th Annual Conference of the EACSL, Lausanne, Switzerland, 11/09/07. https://doi.org/10.1007/978-3-540-74915-8_21

A soft type assignment system for λ-calculus. / Gaboardi, Marco; Della Rocca, Simona Ronchi.
Computer Science Logic: 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007. Proceedings. ed. / Jacques Duparc; Thomas A. Henzinger. Berlin: Springer , 2007. p. 253-267 (Lecture notes in computer science; Vol. 4646).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - A soft type assignment system for λ-calculus

AU - Gaboardi, Marco

AU - Della Rocca, Simona Ronchi

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

KW - LAMBDA-CALCULUS

KW - POLYNOMIAL-TIME

KW - LINEAR LOGIC

U2 - 10.1007/978-3-540-74915-8_21

DO - 10.1007/978-3-540-74915-8_21

M3 - Conference contribution

SN - 9783540749141

T3 - Lecture notes in computer science

SP - 253

EP - 267

BT - Computer Science Logic

A2 - Duparc, Jacques

A2 - Henzinger, Thomas A.

PB - Springer

CY - Berlin

T2 - 21st International Workshop on Computer Science Logic, CSL 2007/16th Annual Conference of the EACSL

Y2 - 11 September 2007 through 15 September 2007

ER -

Gaboardi M, Della Rocca SR. A soft type assignment system for λ-calculus. In Duparc J, Henzinger TA, editors, Computer Science Logic: 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007. Proceedings. Berlin: Springer . 2007. p. 253-267. (Lecture notes in computer science). doi: 10.1007/978-3-540-74915-8_21

A soft type assignment system for λ-calculus

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this