Curry-Howard Correspondence
The deep structural identity between proofs and programs (Curry 1934, Howard 1969): propositions correspond to types, proofs to programs, and proof normalisation to program execution. The intuitionistic logic / simply-typed λ-calculus correspondence is the classical case. Linear-logic Curry–Howard (Caires & Pfenning 2010, Wadler 2012) extends the correspondence to concurrency: Linear Logic propositions ⇔ Session Types, proofs ⇔ Pi-Calculus processes, cut elimination ⇔ communication. The result is a typed concurrent calculus in which deadlock-freedom and session fidelity are corollaries of cut elimination.