On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus
This program is tentative and subject to change.
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 JanDisplayed time zone: Mountain Time (US & Canada) change
15:00 - 16:20 | |||
15:00 20mTalk | The Duality of λ-Abstraction POPL | ||
15:20 20mTalk | On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus POPL Naoki Kobayashi University of Tokyo | ||
15:40 20mTalk | 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 20mTalk | 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 |