A Complementary Approach to Incorrectness Typing
summary
A two-sided type system treats types as sets of normal forms rather than values and introduces a complement operator that behaves like logical negation on typing formulas. The system derives refutation principles including a type-theoretic co-implication, uses a decidable subtyping axiomatization to encode the complement, and certifies several Erlang-like programs as definitely going wrong. The metatheory proves soundness and completeness for normal forms; no implementation is reported.
AI-written summary · about
chapters (19)
- 0:00Incorrectness typing intro
- 1:00Motivation for correctness/incorrectness types
- 3:09Defining program failures
- 6:13Normal forms: values vs stuck terms
- 7:40Types as sets of normal forms
- 9:13Complement operator necessity
- 11:30Set-theoretic reasoning tools
- 13:17Subtyping and complement intuition
- 14:46Reputation principles constraints
- 17:20Preservation and progress proofs
- 18:05Two-sided typing system
- 20:37Deriving left rules from complement
- 22:06Two-sided judgments as proofs
- 24:16Connection to bi-intuitionistic logic
- 25:48Sequent-style term typing
- 26:33Composing necessity types challenges
- 27:18Co-arrow type for refutation
- 28:24Key messages summary
- 29:11Q&A
related talks
19mIll-Typed Programs Don't Evaluate
46mThe Calculated Typer (Functional Pearl)
52mType Theory and its Meaning Explanations
17mFrom Traces to Program Incorrectness: A Type-Theoretic Approach
56mOn Type-Based Techniques for Program Manipulation
53mIntroduction to Intuitionistic Type Theory
48mA History of Subtyping
20mImperative Compositional Programming: Type Sound Distributive Intersection Subtyping(…)