Lectures on Linear Logic

✍ Scribed by A. S. Troelstra

• Publisher: Center for the Study of Language and Inf
• Year: 1992
• Tongue: English
• Leaves: 216
• Series: Lecture Notes
• Edition: 1
• Category: Library

✦ Synopsis

The initial sections of this text deal with syntactical matters such as logical formalism, cut-elimination, and the embedding of intuitionistic logic in classical linear logic. Concluding chapters focus on proofnets for the multiplicative fragment and the algorithmic interpretation of cut-elimination in proofnets.

✦ Table of Contents

1 Introduction 1
2 Sequent calculus for linear logic 15
3 Some elementary syntactic results 26
4 The calculus of two implications: a digression 41
5 Embeddings and approximations 45
6 Natural deduction systems for linear logic 56
7 Hilbert-type systems 65
8 Algebraic semantics 71
9 Combinatorial linear logic 81
10 Girard domains 92
11 Coherence in symmetric monoidal categories 102
12 The storage operator as a cofree comonoid 111
13 Evaluation in typed calculi 119
14 Computation by lazy evaluation in CCC's 125
15 Computation by lazy evaluation in SMC's and ILC's 134
16 The categorical and linear machine 139
17 Proofnets for the multiplicative fragment 144
18 The algorithm of cut elimination for proof nets 155
19 Multiplicative operators 162
20 The undecidability of linear logic 172
21 Cut elimination and strong normalization 179
References 191
Index 197

✦ Subjects

Combinatorics;Pure Mathematics;Mathematics;Science & Math;Logic;Pure Mathematics;Mathematics;Science & Math