Tue 22 Oct 2024 14:45 - 15:10 at Pasadena - Afternoon Paper Session

In a POPL 2016 paper, Brown and Palsberg presented a breakthrough result on “the normalization barrier.” The normalization barrier, according to conventional wisdom, originates from a theorem in computability theory, which says that a total universal function for all total computable functions is impossible. Therefore, it was widely believed that strongly normalizing lambda calculi do not have self-interpreters either. However, Brown and Palsberg constructed a self-interpreter for F-omega, which is a strongly normalizing lambda calculus. One of the key insights behind the Brown-Palsberg breakthrough is due to the fact that ``static type checking in F-omega can exclude the (computability) proof’s diagonalization gadget, leaving open the possibility for a self-interpreter,'' according to Brown and Palsberg [2016].

In this paper, we revisit this phenomenon. In particular, in the Brown-Palsberg result, terms in F-omega were encoded as typed representations, and an external type checker was assumed to do type checking. In our work, we consider a type checker assumed to be built into the interpreter, which reports type errors on ill-typed inputs. We believe this is closer to real interpreters. Consequently, our representation is untyped, and ill-typed inputs are permitted. Under this setting, we show that the original computability theory result still holds. Our result does not contradict the Brown-Palsberg result. Rather, it shows that computability theory results are still applicable to F-omega from a different angle, thus ``rebuilding'' the normalization barrier.

Tue 22 Oct

Displayed time zone: Pacific Time (US & Canada) change

14:00 - 15:30
Afternoon Paper SessionJENSFEST at Pasadena
14:00
20m
Keynote
Jens, the Ultimate PL Renaissance man!
JENSFEST
Vivek Sarkar Rice University, USA
14:20
25m
Talk
The Essence of the Flyweight Design Pattern
JENSFEST
Fernando Magno Quintão Pereira Federal University of Minas Gerais, Caio Raposo Universidade Federal de Minas Gerais
14:45
25m
Talk
The Normalization Barrier Revisited
JENSFEST
Shuo Ding Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology
15:10
20m
Talk
Input Reduction with Reduction Trees
JENSFEST
Christian Gram Kalhauge Technical University of Denmark