Keynote: Propositions as Types
summary
The principle propositions as types asserts a tight isomorphism: natural deduction ↔ typed lambda calculus, proofs ↔ programs, normalization ↔ evaluation. Consequence: typed programs always terminate (so they cannot express every Turing-computable function unless recursion or paradoxical encodings are reintroduced). Concrete tooling and lineage appear: Hindley–Milner and System F type systems, monads and continuation‑passing style, dependent types and proof assistants. Practical outcome: verified artifacts (for example Coq proof of the four color theorem) and session‑type protocols from linear logic for concurrency.
AI-written summary · about
chapters (17)
- 0:00Start
- 3:15Girdle Numbering
- 5:01Lambda Calculus
- 8:14Turing Machines
- 11:21Basic Natural Deduction
- 14:35Prove an Implication
- 15:21The Sub Formula Property
- 26:04Evaluating a Program
- 27:55The Curry Howard Isomorphism
- 31:20Type Abstraction
- 31:46Modal Logic
- 40:28Multiverses
- 46:07Recommendations for Things To Read
- 48:53Logic Comics
- 49:41Linear Logic
- 50:47Syntactic Control of Interference
- 51:39What Logical System Does Untyped Lambda Calculus Correspond to
related talks
01h 12mTruth about Types
47mHistory and Philosophy of types
01h 57mTypes as Program Specifications: A Intro to Type-Level Programming in Haskell
56mWrite You Some Proofs for Great Good
49mThe Trouble With Types
39mCommunicating in Types
36mCommunicating in Types
28mType-Driven Prompt Programming: From Typed Interfaces to a Calculus of Constraints