Why Are Proofs Relevant in Proof-Relevant Models?
summary
Categorifying relational graph models using distributors yields categorified graph models whose denotations are distributors returning full type derivations not just typings, i.e., proof-relevant interpretations. The paper proves a categorical Approximation Theorem: a term’s semantics is the filtered colimit of its finite approximants, and every derivation reconstructs a matching approximant. Consequences: strong normalization and confluence of reduction on derivations, and the induced (non‑extensional) equational theory coincides with equality of Böhm trees.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:15Scott Semantics
- 1:49Scott / Relational Semantics
- 2:22Scott / Relational / Bicategorical Semantics
- 3:20Denotational Semantics
- 4:25A Syntax for Semantics
- 6:14Infinite Normal Forms: Böhm Trees
- 8:39Relational Graph Models
- 11:27Categorified Graph Models
- 12:55Categorifying Intersection Types
- 13:51Denotations are Distributors
- 15:58Normalization of the semantics
- 19:21Perspectives
- 21:01Derivations Under Reduction
related talks
34mFormalizing the ∞-categorical Yoneda lemma
14mAdequacy for Algebraic Effects Revisited
18mCompleteness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq
14mA Limited Case for Reification by Type Inference
52mType Theory and its Meaning Explanations
28mTowards Light-Weight Operational Reasoning for Languages with Binders, Categorically
23mFrom Semantics to Syntax: A Type Theory for Comprehension Categories
24mA Computational Interpretation of Compact Closed Categories