Type Theory and its Meaning Explanations
summary
Argues that verification not proof is the core notion, and builds a semantics where types are sets of canonical verifications with equivalence; uses meaning explanations, lazy evaluation, canonical forms and a new sequent/context machinery to define unit and dependent function (Pi) types. Shows a concrete construction and inversion proofs that make admissible elimination rules follow rather than be axiomatic, fixes extensionality problems that would force excluded middle, and demonstrates the approach succeeds with a small, modular metatheory.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 1:34Evaluation judgment
- 6:20Categorical judgment
- 11:00Highorder judgment
- 24:48Contexts
- 31:48Computation
- 39:28Evidence
related talks
19mIll-Typed Programs Don't Evaluate
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
19mExtensible Metatheory Mechanization via Family Polymorphism
19mType Inference Logics
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
11mLocal algebraic effect theories
52mWhat logic can teach us, Scala programmers
46mThe Calculated Typer (Functional Pearl)