THE LIVING ARCHIVE

From punched cards to autonomous collaborators: the ideas, people, languages and systems that taught machines to follow—and increasingly interpret—human intent.

PAST / PRESENT / NEXT

Collection

Tag: propositions-as-types

Per Martin-Löf and Dependent Type Theory: Programs, Propositions, and Proofs

Per Martin-Löf's intuitionistic type theory made types expressive enough to depend on values, linking programs, mathematical propositions, and constructive proofs in one formal language.

↗