The Normalization Barrier Revisited
summary
Revisits Brown and Palsberg’s POPL 2016 result and shows that if the interpreter embeds type checking and accepts untyped representations (Church numerals encoding programs) then a total self-evaluator cannot exist: the paper builds a numeric encoding, an apply concatenation primitive, and requires the representation larger than numeral property, then runs a diagonal construction that yields the contradiction (a number greater than itself plus one). Result: allowing type-error outputs restores the classic computability impossibility.
AI-written summary · about
chapters (8)
- 0:00Normalization barrier intro
- 1:47Normalization barrier revisited
- 3:57Defining interpreters
- 6:30Diagonal argument & self-interpreters
- 8:39Type representations & limits
- 10:05Encoding errors in evaluators
- 13:45Key takeaways
- 14:52Q&A on type expressiveness
related talks
23mNormalizable types
35mPractical Normalization by Evaluation for EDSLs
19mIll-Typed Programs Don't Evaluate
14mA dependently typed calculus with pattern matching and erasure inference
01h 01mA partial history of partial evaluation
01h 03mVerifying Dependent Type-checkers
14mAdequacy for Algebraic Effects Revisited
01h 07mInvited Talk - Guy Steele