Reference. One Weird Trick to Untie Landin’s Knot

In this work, we explore Landin’s Knot, which is understood as a pattern for encoding general recursion, including non-termination, that is possible after adding higher-order references to an otherwise terminating language. We observe that this isn’t always true – higher-order references, by themselves, don’t lead to non-termination. The key insight is that Landin’s Knot relies not primarily on references storing functions, but on unrestricted quantification over a function’s environment. We show this through a closure converted language, in which the function’s environment is made explicit and hides the type of the environment through impredicative quantification. Once references are added, this impredicative quantification can be exploited to encode recursion. We conjecture that by restricting the quantification over the environment, higher-order references can be safely added to terminating languages, without resorting to more complex type systems such as linearity, and without restricting references from storing functions.

Cite

Cite as @koronkevich-2025-one (helia, typst) · \cite{koronkevich-2025-one} (LaTeX)
BibTeX
bibtex · 8 lines
@misc{koronkevich-2025-one,
  author = {Paulette Koronkevich and William J. Bowman},
  title = {One Weird Trick to Untie Landin’s Knot},
  year = {2025},
  month = {7},
  eprint = {2507.21317},
  archiveprefix = {arXiv}
}
hayagriva YAML (typst)
yaml · 9 lines
koronkevich-2025-one:
  type: misc
  title: One Weird Trick to Untie Landin’s Knot
  author:
  - Koronkevich, Paulette
  - Bowman, William J.
  date: 2025-07
  serial-number:
    arxiv: '2507.21317'
Cites 11 works (3 here)
With notes (3)

Syntax and Semantics of Quantitative Type Theory atkey-2018-syntax

DOI

I Got Plenty o’ Nuttin’ mcbride-2016-i

DOI

Integrating Linear and Dependent Types krishnaswami_integrating_2015

In this paper, we show how to integrate linear types with type dependency, by extending the linear/non-linear calculus of Benton to support type dependency.
PDF · DOI · pldb
koronkevich-2025-one reference entries/refs/koronkevich-2025-one/koronkevich-2025-one.hel