POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Wed 14 Jan 2026 10:55 - 11:20 at Nef - Functional Programming Chair(s): Alex Rice

Metaprogramming and effect handlers interact in unexpected, and sometimes undesirable, ways. One example is scope extrusion: the generation of ill-scoped code. Scope extrusion can either be preemptively prevented, via static type systems, or retroactively detected, via dynamic checks. Static type systems exist in theory, but struggle with a range of implementation and usability problems in practice. In contrast, dynamic checks exist in practice (e.g. in MetaOCaml), but are understudied in theory. Designers of metalanguages are thus given little guidance regarding the design and implementation of checks. We present the first formal study of dynamic scope extrusion checks, introducing a calculus ($\lambda_{\langle\langle\text{op}\rangle\rangle}$) for describing and evaluating checks. Further, we introduce a novel dynamic check — the “Cause-for-Concern” check — which we prove correct, characterise without reference to its implementation, and argue combines the advantages of existing dynamic checks. Finally, we extend our framework with refined environment classifiers, which statically prevent scope extrusion, and compare their expressivity with the dynamic checks.

Wed 14 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

10:30 - 12:10
Functional Programming POPL at Nef
Chair(s): Alex Rice University of Edinburgh
10:30
25m
Talk
Domain-Theoretic Semantics for Functional Logic Programming
POPL
Eddie Jones University of Bristol, Samson Main University of Bristol, Celia Mengyue Li University of Bristol, Jonathan Marriott University of Bristol, Alex Kavvos University of Bristol
DOI
10:55
25m
Talk
Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks
POPL
Michael Lee University of Cambridge, UK, Ningning Xie University of Toronto, Oleg Kiselyov Tohoku University, Jeremy Yallop University of Cambridge
DOI
11:20
25m
Talk
Hyperfunctions: Communicating Continuations
POPL
Donnacha Oisín Kidney Imperial College London, Nicolas Wu Imperial College London
DOI Pre-print
11:45
25m
Talk
Lazy Linearity for a Core Functional Language
POPL
Rodrigo Mesquita Well-Typed LLP, Bernardo Toninho Instituto Superior Técnico - University of Lisbon
DOI Pre-print