Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework
summary
Proves decidability of inhabitation for a unifying calculus lambda! by using non-idempotent intersection types to extract quantitative bounds (reduction length and size) and by computing a finite basis that generates all inhabitants; gives an algorithm that terminates, is complete for that basis, and is implemented. Shows embeddings of call-by-name and call-by-value into the framework preserve typability so the same inhabitation procedure yields decidability for those calculi, and explains how grammar-driven generation and restriction recover only the desired term shapes.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:10Inhabitation significance
- 3:02Distant lambda calculus
- 4:49Embedding calculi
- 5:53Quantitative types
- 7:55Decidability in lambda
- 9:22All inhabitation solutions
- 11:12Finite basis construction
- 13:19Algorithm details
- 15:53Grammar restrictions
- 17:38Results and future
- 20:00Q&A
related talks
22mA Calculus of Inductive Linear Constructions
15mStable Relations and Abstract Interpretation of Higher-Order Programs
18mMulti Types and Reasonable Space
42mWould Aliens Understand Lambda Calculus
31mDependent tagless final
21mQuantum and Classical Control (work-in-progress)
14mAdequacy for Algebraic Effects Revisited
30mNormalisation for First-Class Universe Levels