The formulae-as-types correspondence is normally understood as giving
a constructive interpretation for a logic, whilst classical logic is
normally understood as resisting an interpreatation. Thus results
that show that classical logic admits a formulae-as-types
correspondence have provoked a lot of interest in the research community.
Applications of logic to process algebras are often inspired by the
concurrent analogue of the formulae-as-types correspondence proposed
by Samson Abramsky and inspired by Girard's linear logic.