Propositions as types

What is it about?

Powerful insights arise from linking two fields of study previously thought separate. Examples include Descartes's coordinates, which links geometry to algebra, Planck's Quantum Theory, which links particles to waves, and Shannon's Information Theory, which links thermodynamics to communication. Such a synthesis is offered by the principle of Propositions as Types, which links logic to computation. At first sight it appears to be a simple coincidence—almost a pun—but it turns out to be remarkably robust, inspiring the design of automated proof assistants and programming languages, and continuing to influence the forefronts of computing.

Featured Image

Why is it important?

Propositions as Types observes a deep correspondence between logic and computation: propositions in a logic correspond to types in a programming language; proofs of propositions correspond to programs of the corresponding type; and simplification of proofs corresponds to evaluation of programs. Propositions as Types is broadly applicable, applying to a wide variety of logics (intuitionistic, second-order, classical, linear) and of language features (lambda calculus parametric polymorphism, continuations, concurrency). Often the same ideas are discovered independently by logicians and computer scientists, demonstrating some aspects of programming language design are not arbitrary but absolute.

Perspectives