Notes - A Taste of Linear Logic

I’ve taken some time between OPLSS lectures to read Philip Wadler’s A Taste of Linear Logic. I’ve filled in enough gaps in my knowledge of logic and type theory over the past week that I can now process dense type system papers. This makes me really happy.

As a part of reading this paper (which is an excellent summary of intuitionistic logic and linear logic), I put together some notes in the form of an org mode file. I’m linking it here in case it’s of use to anyone else.

Notes: Link

Happy reading!

Thoughts

I’m interested in understanding linear logic better. I think it’s really powerful to give users of a programming language the option of handling segments of their programs as resources. I feel like linear logical constraints (LLC) as a first class citizen of a language would lead to:

• Better error messages when those constraints aren’t satisfied
• General availability of these tools for the development of programs
• A run-time system that can optimize segments of the program involving LLC

What do I mean by resources? Things like:

• Memory
• Files
• Sockets
• Streams
• Sessions
• Transactions
• Locking Primitives

There’s a lot to unpack in the literature of linear logic. A good starting point from the programming point of view is to see what the Rust programming language has done, or nearly any paper on session types.

Notation

I use a type-signature-like notation for logical rules to make them easier to translate to this textual medium. For example:

Γ ⊢ A  Δ ⊢ B
------------ (×-I)
Γ,Δ ⊢ A × B

Becomes:

×-I : ⟦(Γ ⊢ A) (Δ ⊢ B)⟧
  ⟶  ⟦(Γ, Δ ⊢ A × B)⟧

The name now comes first, rather than being off to the side. The required assumtions start the type signature, and the conclusion becomes the “return” of the type. It’s a take on propositions-as-types for the sake of facilitating my note taking.