Cover Image
QR Code

Propositions as Types.

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...

Full description

Published in:Communications of the ACM Vol. 58; no. 12; pp. 75 - 85
Main Author: WADLER, PHILIP
Format: Article
Published: Association for Computing Machinery Dec2015
Subjects:
Mathematical logic
Computer programming
Proposition (Logic)
Mathematical proofs
Data types (Computer science)
Computer software
Online Access:View this record in EBSCOhost
Summary: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.