POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Tue 16 Jan 2024 10:05 - 10:30 at Haslett Room - Keynote & Termination analysis Chair(s): Meng Wang

A program generating a co-inductive data structure is called productive if the program eventually generates all the elements of the data structure. We propose a new method for verifying the productivity, which transforms a co-inductive data structure into a function that takes a path as an argument and returns the corresponding element. For example, an infinite binary tree is converted to a function that takes a sequence consisting of 0 (left) and 1 (right), and returns the element in the specified position, and a stream is converted into a function that takes a sequence of the form 0^n (or, simply a natural number n) and returns the n-th element of the stream. A stream-generating program is then productive just if the function terminates for every n. The transformation allows us to reduce the productivity verification problem to the termination problem for call-by-name higher-order functional programs without co-inductive data structures. We formalize the transformation and prove its correctness. We have implemented an automated productivity checker based on the proposed method, by extending an automated HFL(Z) validity checker, which can be used as a termination checker.

Tue 16 Jan

Displayed time zone: London change

09:00 - 10:30
Keynote & Termination analysis PEPM at Haslett Room
Chair(s): Meng Wang University of Bristol
Meng Wang University of Bristol, Gabriele Keller Utrecht University
From Theory to Practice: Crafting Differential Privacy Systems with Haskell
Alejandro Russo Chalmers University of Technology, Sweden
Productivity Verification for Functional Programs by Reduction to Termination Verification
Ren Fukaishi The University of Tokyo, Naoki Kobayashi University of Tokyo, Ryosuke Sato University of Tokyo