POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States

This program is tentative and subject to change.

Fri 24 Jan 2025 15:20 - 15:40 at Room 2 - Theory

The decidability of the reachability problem for finitary PCF has been used as a theoretical basis for fully automated verification tools for functional programs. The reachability problem, however, often becomes undecidable for a slight extension of finitary PCF with side effects, such as exceptions, algebraic effects, and references, which hindered the extension of the above verification tools for supporting functional programs with side effects. In this paper, we first give simple proofs of the undecidability of four extensions of finitary PCF, which would help us understand and analyze the source of undecidability. We then focus on an extension with references, and give a decidable fragment using a type system. To our knowledge, this is the first non-trivial decidable fragment that features higher-order recursive functions containing reference cells.

This program is tentative and subject to change.

Fri 24 Jan

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

15:00 - 16:20
TheoryPOPL at Room 2
15:00
20m
Talk
The Duality of λ-Abstraction
POPL
Vikraman Choudhury Università di Bologna & Inria OLAS, Simon J. Gay University of Glasgow, UK
15:20
20m
Talk
On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus
POPL
Naoki Kobayashi University of Tokyo
15:40
20m
Talk
Interaction Equivalence
POPL
Beniamino Accattoli Inria & Ecole Polytechnique, Adrienne Lancelot Inria, LIX Ecole Polytechnique, IRIF Université Paris Cité, Giulio Manzonetto Université Paris Cité, Gabriele Vanoni IRIF, Université Paris Cité
16:00
20m
Talk
Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings
POPL
Jan van Brügge Heriot-Watt University, James McKinna Heriot-Watt University, Andrei Popescu University of Sheffield, Dmitriy Traytel University of Copenhagen