Typing Strictness
summary
Proposes a refinement of strictness called intentional strictness and encodes it as a type-and-effect system for call-by-name and call-by-push-value, with a strictness-annotation-preserving translation between them. Proves via a logical relation that intentionally strict variables are always scrutinized and intentionally lazy ones are never scrutinized (properties named strict failure and lazy soundness), mechanizes the proofs and translation in Rocq, and ships evaluated artifacts and a paper DOI for full definitions and examples.
AI-written summary · about
chapters (13)
- 0:00Typing strictness introduction
- 1:05Strict vs lazy evaluation
- 3:09Variable usage patterns
- 5:36Usage and evaluation link
- 7:43Extensional strictness in functions
- 9:50Challenges with extensional strictness
- 11:57Intentional strictness definition
- 13:00Strict positions syntax
- 14:04Type and effect system
- 16:31Intentional strictness properties
- 19:24Benefits of intentional strictness
- 20:47Future work and paper
- 21:14Q&A
related talks
24mCatching space leaks at compile-time using th-deepstrict
46mThe Calculated Typer (Functional Pearl)
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
52mType Theory and its Meaning Explanations
24mTyped Equivalence of Labeled Effect Handlers and Labeled Delimited Control Operat...
45mTDD, as in Type-Directed Development
31mDependently-Typed Programming with Logical Equality Reflection
28mLanguage Support for Property-Based Testing