What is the Curry-Howard analogue for linear logics?
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).