Papers for
functional programming language designers
Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.
Explicit bounds on complexity of System T dialogue trees below epsilon naught
An Explicit Ordinal Bound for System T Dialogue Trees
Abstract: Escardó's dialogue interpretation assigns to each closed term $t:(ι\toι)\toι$ of Gödel's System~T a well-founded, countably branching tree $D(t)$, where $ι$ is the natural-number type. We give a direct proof that its classical ordinal height is below $ε_0$. More precisely, we compute a natural number $K(t)\ge2$ from the type levels occurring in the source term and prove $h(D(t))<θ_{K(t)}$, where $θ_0=ω$ and $θ_{n+1}=ω^{θ_n}$. Our proof translates recursors into closed infinitary templates and eliminates $β$-redexes by a finite sequence of passes indexed by ordinary type level. The translation and every pass preserve the dialogue denotation exactly. An auxiliary rank $ρ$ satisfies an additive substitution bound; each pass sends rank $α$ to at most $2^α$. Combining these estimates with a computable initial bound $ω+m(t)$ and a dialogue-height bound $2^{ρ(N)}$ for closed ground normal forms $N$ yields the stated tower bound. A semantics-preserving translation transfers the result to Escardó's original combinatory interpretation. We formalise the proof in Agda over classical ordinals under explicit foundational assumptions.
New relationship between models improves planar lambda calculus theory
On Models of the Planar Lambda Calculus
Abstract: We construct an adjunction relating two approaches to modelling the planar lambda calculus: semi-closed operads and planar lambda-models. We use this to obtain a planar version of Scott's representation theorem.