What is the Curry-Howard analogue for linear logics?

Question

As defined by Wikipedia,

(The Curry-Howard correspondence) is a generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the American mathematician Haskell Curry and logician William Alvin Howard.

Related to it is the λ-cube, which is a graphical representation of the possible axes of refinement from simple types to the calculus of constructions, which has a logical interpretation:

As far as I know, the Curry-Howard correspondence is a connection between type theory and classical logics. My question is: is there any analogue correspondence between type systems and linear logics?

Answer 1

Linear logic corresponds to a type system for a process calculus (a variant of the internal π-calculus), where:

• proofs correspond to processes;
• propositions correspond to session types (communication protocols).

This is a pretty active area of research. While people expected a correspondence between linear logic and some concurrency model since the inception of linear logic by Girard [1987], finding something that is satisfying from both the logical and the concurrency modelling perspectives has been somewhat elusive.

Here is a summary of the key developments so far.

• Abramsky [1994] and Bellin and Scott [1994] proposed the first "Proofs as Processes" correspondence, where linear propositions are types for linear channels in a process calculus. For example, the proposition $A \otimes B$ is interpreted as the channel type "send $A$ and $B$"; it is used to type a process that uses a channel to output a message including something of type $A$ and $B$ (a pair, if you like), respectively, and then the channel must not be used anymore. The key idea is that the cut rule of linear logic can be used to type the parallel execution of two processes that communicate over a private channel. The duality check performed by the cut rule in linear logic corresponds to checking that the two processes use the shared private channel in compatible ways.
• The idea of duality inspired also several typing disciplines for process calculi, most notably linear types and session types, but the direct link to linear logic was lost. Session types in particular, by Honda [1993], describe communication protocols and their applicability became evident pretty soon: the idea spawned a research area.
• Seven years later after Honda developed session types, Caires and Pfenning [2010] found that propositions in intuitionistic linear logic can be interpreted as session types. For example, the proposition $A \otimes B$ is interpreted as the protocol "send $A$ and then proceed as $B$". This discovery has rejuvenated the "Proofs as Processes" research line: there are a lot of papers on this topic published in the last decade. Thanks to the logical foundations, we can import ideas from logic for extending the typing discipline of session types.
• Wadler [2014] reformulated the correspondence with session types for classical linear logic and formalised the first connection between a standard presentation of session types for a functional language and linear logic.
• There is an "issue" shared by all the works cited above: while the linear logic side is the expected one, the process calculus side is not, both syntactically and semantically. For example, a notable discrepancy is that parallel composition ($P|Q$) is not a standalone term constructor, because it lacks a corresponding rule for reasoning about it directly in linear logic. This issue has been resolved in [Kokke et al., 2019] (disclaimer: I'm one of the authors), by conservatively reformulating the rules for $\otimes$, cut, and mix. This gives rise to new proof transformations, which turn out to correspond to the expected observational semantics of the π-calculus.

If you're looking for a couple of papers to get started, I would start from [Wadler, 2014] and then [Kokke et al., 2019] (to see the latest system).

Answer 2

You can impose similar requirements within your type system, which amounts to requiring that objects never be destroyed nor duplicated. For an example of a practical application, see Linear Types can Change the World! by Philip Wadler, which specifies typing rules for this. It also shows how a type system can combine linear and non-linear types.

For a practical application of this, take a look at std::unique_ptr in C++. Here, linearity ensures that deallocation always occurs exactly once.

In a functional language, linearity also gives the possibility of destructive updates (that appear pure to the programmer). However, in practice it seems like monads are a more common approach to solving this problem.

Update: I noticed that in the NLab Computational Trinitarianism table the absence of contraction in a logic (i.e. being unable to duplicate an assumption) corresponds to the No-Cloning Theorem from quantum mechanics. I (unfortunately) don't understand the implications of this, but I thought you might find it interesting.