For almost 100 years, there have been linkages forged between certain notions of logic and of computation. As more associations have been discovered, the bonds between the two have grown stronger and richer.

• Propositions in logic can be considered equivalent to types in programming languages.
• Proofs of propositions in logic can be considered equivalent to programs of given type in computation.
• The simplification of proofs of propositions in logic can be considered equivalent to the evaluation of programs of types in computation.

The separate work of various logicians and computer scientists (and their precursors) can be paired:

• Gerhard Gertzen’s work on proofs in intuitionistic natural deduction and Alonzo Church’s work on the simply typed lambda calculus.
• J. Roger Hindley and Robin Milner’s work on type systems for combinatory logic and programming languages, respectively.
• J. Y. Girard and John Reynold’s work on the second order lambda calculus and parametric polymorphic programs, respectively.
• Haskell Curry’s and W. A. Howard’s work on the overall correspondence between these notions of proofs as programs or positions as types.

Logic and computation are the sequential chains of efficient causation and actions. Propositions and types are the abstract grids of formal causation and structures. Proofs and programs are the normative cycles of final causation and functions. Simplification and evaluation are the reductive solids of material causation and parts.

References:

Philip Wadler / Propositions as Types, in Communications of the ACM, Vol. 58 No. 12 (Dec 2015) Pages 75-85.

http://cacm.acm.org/magazines/2015/12/194626-propositions-as-types/fulltext

Preprint at

Click to access propositions-as-types.pdf

Also see:

http://www.drdobbs.com/old-ideas-form-the-basis-of-advancements/184404384

https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system

https://en.wikipedia.org/wiki/System_F

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence

[*9.92-9.94]

<>