Thu 19 Jan 2023 10:20 - 10:45 at Avenue34 - Semantics I Chair(s): Neel Krishnaswami

This paper proposes a new approach to writing and verifying
divide-and-conquer programs in Coq. Extending the rich line of
previous work on algebraic approaches to recursion schemes, we
present an algebraic approach to divide-and-conquer recursion:
recursions are represented as a form of algebra, and from outer
recursions, one may initiate inner recursions that can construct
data upon which the outer recursions may legally
recurse. Termination is enforced entirely by the typing discipline
of our recursion schemes. Despite this, our approach requires little
from the underlying type system, and can be implemented in System
$F_\omega$ plus a limited form of positive-recursive types. Our
implementation of the method in Coq does not rely on structural
recursion or on dependent types. The method is demonstrated on
several examples, including mergesort, quicksort, Harper's
regular-expression matcher, and others. An indexed version is also
derived, implementing a form of divide-and-conquer induction that
can be used to reason about functions defined via our method.

Thu 19 Jan

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

10:20 - 12:00
Semantics IPOPL at Avenue34
Chair(s): Neel Krishnaswami University of Cambridge
10:20
25m
Talk
A Type-Based Approach to Divide-and-Conquer Recursion in Coq
POPL
Pedro da Costa Abreu Junior Purdue University, Benjamin Delaware Purdue University, Alex Hubers University of Iowa, Christa Jenkins University of Iowa, J. Garrett Morris University of Iowa, Aaron Stump University of Iowa
DOI
10:45
25m
Talk
Elements of Quantitative RewritingVirtual
POPL
Francesco Gavazzo University of Pisa, Cecilia Di Florio University of Bologna
DOI
11:10
25m
Talk
The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding
POPL
Simon Castellan University of Rennes; Inria; CNRS; IRISA, Pierre Clairambault Université Aix-Marseille; Université de Toulon; CNRS; LIS
DOI
11:35
25m
Talk
Deconstructing the Calculus of Relations with Tape Diagrams
POPL
Filippo Bonchi University of Pisa, Alessandro Di Giorgio University of Pisa, Alessio Santamaria University of Pisa; University of Sussex
DOI