Generating Well-Typed Terms that are not "Useless"
summary
Generates well typed lambda terms that intentionally delay choosing argument types by introducing extension variables and an extensible application rule, implemented as mutable pointers into an OCaml generator. Formal step-relations and proofs show nonlocal extension steps preserve typing. Evaluation reproduces prior GHC bug-finding results faster, raises function-parameter usage from about 30% used (70% unused) to roughly 55% used, and ships artifacts and a reusable implementation.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 1:28Differential compiler testing
- 3:34Stochastic term generation
- 5:06Useless function arguments
- 6:29Extension variables
- 9:04Formalizing extension variables
- 11:55Revisiting generation example
- 13:03Summary
- 14:29Implementation details
- 14:51Q&A
- 15:15Evaluation results
- 16:18Repeated variable usage
- 16:39Effectiveness measurement
- 17:46OCaml implementation
- 18:48Testing type checkers
- 19:09Final Q&A
related talks
30mConstrained generation of well-typed programs
15mType-safe generation of modules in applicative and generative styles
28mSemi-explicit polymorphic parameters
56mOn Type-Based Techniques for Program Manipulation
22mType-Safe Code Generation With Algebraic Effects and Handlers
18mDeveloping a Dependently Typed Language with Runtime Proof Search
15mElaboration with First-Class Implicit Function Types
18mDeferring the Details and Deriving Programs