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?