Propositions as Types. - WADLER, PHILIP (Communications of the ACM, 2015)
The article presents the Propositions as Types model, which attempts to conceptually link mathematical logic with computation. Topics addressed include an overview of several corresponding features of both systems, such as propositions proofs and simplification to types, programs and evaluation; how the independent overlapping discoveries by both groups reinforce their findings, and how this model can extend to other forms of logic.