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.
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:
What do I mean by resources? Things like:
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.
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
×-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.