ICFP 2023
Mon 4 - Sat 9 September 2023 Seattle, Washington, United States
Mon 4 Sep 2023 09:00 - 09:30 at Vashon - HOPE: Session 1 Chair(s): Max S. New

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.

Mon 4 Sep

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

09:00 - 10:30
HOPE: Session 1HOPE at Vashon
Chair(s): Max S. New University of Michigan
09:00
30m
Talk
One Weird Trick to Untie Landin's Knot
HOPE
Paulette Koronkevich University of British Columbia, William J. Bowman University of British Columbia
09:30
30m
Talk
Operational game semantics for generative algebraic effects and handlersRemote
HOPE
Hamza Jaâfar Inria, Guilhem Jaber Nantes Université
10:00
30m
Talk
Higher-Order Weakest Precondition Transformers via a CPS Transformation
HOPE
Satoshi Kura National Institute of Informatics
Pre-print