A Syntax for Linear Logic

Philip Wadler

doi:10.1007/3-540-58027-1_24

A Syntax for Linear Logic

Philip Wadler

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

Abstract

There is a standard syntax for Girard's linear logic, due to Abramsky, and a standard semantics, due to Seely. Alas, the former is incoherent with the latter: different derivations of the same syntax may be assigned different semantics. This paper reviews the standard syntax and semantics, and discusses the problem that arises and a standard approach to its solution. A new solution is proposed, based on ideas taken from Girard's Logic of Unity. The new syntax is based on pattern matching, allowing for concise expression of programs.

Original language	English
Title of host publication	Mathematical Foundations of Programming Semantics
Subtitle of host publication	9th International Conference New Orleans, LA, USA, April 7–10, 1993 Proceedings
Editors	Stephen D. Brookes, Michael G. Main, Austin Melton, Michael W. Mislove, David A. Schmidt
Publisher	Springer
Pages	513-529
Number of pages	17
ISBN (Electronic)	978-3-540-48419-6
ISBN (Print)	978-3-540-58027-0
DOIs	https://doi.org/10.1007/3-540-58027-1_24
Publication status	Published - 1993

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin / Heidelberg
Volume	802
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/3-540-58027-1_24

Cite this

Wadler, P. (1993). A Syntax for Linear Logic. In S. D. Brookes, M. G. Main, A. Melton, M. W. Mislove, & D. A. Schmidt (Eds.), Mathematical Foundations of Programming Semantics: 9th International Conference New Orleans, LA, USA, April 7–10, 1993 Proceedings (pp. 513-529). (Lecture Notes in Computer Science; Vol. 802). Springer. https://doi.org/10.1007/3-540-58027-1_24

@inproceedings{ca190df49dac4c8b81f00c4983257a25,

title = "A Syntax for Linear Logic",

abstract = "There is a standard syntax for Girard's linear logic, due to Abramsky, and a standard semantics, due to Seely. Alas, the former is incoherent with the latter: different derivations of the same syntax may be assigned different semantics. This paper reviews the standard syntax and semantics, and discusses the problem that arises and a standard approach to its solution. A new solution is proposed, based on ideas taken from Girard's Logic of Unity. The new syntax is based on pattern matching, allowing for concise expression of programs.",

author = "Philip Wadler",

year = "1993",

doi = "10.1007/3-540-58027-1\_24",

language = "English",

isbn = "978-3-540-58027-0",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "513--529",

editor = "Brookes, \{Stephen D.\} and Main, \{Michael G.\} and Austin Melton and Mislove, \{Michael W.\} and Schmidt, \{David A.\}",

booktitle = "Mathematical Foundations of Programming Semantics",

address = "United Kingdom",

}

A Syntax for Linear Logic. / Wadler, Philip.
Mathematical Foundations of Programming Semantics: 9th International Conference New Orleans, LA, USA, April 7–10, 1993 Proceedings. ed. / Stephen D. Brookes; Michael G. Main; Austin Melton; Michael W. Mislove; David A. Schmidt. Springer, 1993. p. 513-529 (Lecture Notes in Computer Science; Vol. 802).

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

TY - GEN

T1 - A Syntax for Linear Logic

AU - Wadler, Philip

PY - 1993

Y1 - 1993

N2 - There is a standard syntax for Girard's linear logic, due to Abramsky, and a standard semantics, due to Seely. Alas, the former is incoherent with the latter: different derivations of the same syntax may be assigned different semantics. This paper reviews the standard syntax and semantics, and discusses the problem that arises and a standard approach to its solution. A new solution is proposed, based on ideas taken from Girard's Logic of Unity. The new syntax is based on pattern matching, allowing for concise expression of programs.

AB - There is a standard syntax for Girard's linear logic, due to Abramsky, and a standard semantics, due to Seely. Alas, the former is incoherent with the latter: different derivations of the same syntax may be assigned different semantics. This paper reviews the standard syntax and semantics, and discusses the problem that arises and a standard approach to its solution. A new solution is proposed, based on ideas taken from Girard's Logic of Unity. The new syntax is based on pattern matching, allowing for concise expression of programs.

U2 - 10.1007/3-540-58027-1_24

DO - 10.1007/3-540-58027-1_24

M3 - Conference contribution

SN - 978-3-540-58027-0

T3 - Lecture Notes in Computer Science

SP - 513

EP - 529

BT - Mathematical Foundations of Programming Semantics

A2 - Brookes, Stephen D.

A2 - Main, Michael G.

A2 - Melton, Austin

A2 - Mislove, Michael W.

A2 - Schmidt, David A.

PB - Springer

ER -

A Syntax for Linear Logic

Abstract

Publication series

Access to Document

Fingerprint

Cite this