Ill-Typed Programs Don't Evaluate
summary
Introduces two-sided type systems as a sequent-style typing calculus with left rules, a top type for "all values", and a new necessity function type that expresses "if output is produced then input had property". Gives a call-by-value semantics, a syntactic progress-and-preservation proof for a variant of Aiken-style data constructors and pattern matching, a case study on precise data-flow typing, an inference algorithm via constraint generation/solving, and the guarantee ill-typed programs don't evaluate.
AI-written summary · about
chapters (8)
- 0:00Motivation and background
- 1:50Two-sided typing judgments
- 3:31Expressive power of the system
- 6:46Sequent calculus rules
- 9:00Necessity function types
- 12:02Reasoning about incorrectness
- 14:19Summary of contributions
- 15:25Question and answer session
related talks
46mThe Calculated Typer (Functional Pearl)
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
56mOn Type-Based Techniques for Program Manipulation
52mType Theory and its Meaning Explanations
30mA Complementary Approach to Incorrectness Typing
41mThe Dialectics of Type-Level Programming
27mTowards Type Debugging using Partial Evaluation
02h 50mIntro to Type Systems and Operational Semantics