Thu 16 Jun 2022 10:40 - 11:00 at Toucan - Analysis Chair(s): Xiaokang Qiu
Thu 16 Jun 2022 22:40 - 23:00 at Toucan - Analysis

We propose a new cyclic proof system for automated, equational reasoning about the behaviour of pure functional programs. The key to the system is the way in which cyclic proof and equational reasoning are mediated by the use of contextual substitution as a cut rule. We show that our system, although simple, already subsumes several of the approaches to implicit induction variously known as “inductionless induction”, “rewriting induction”, and “proof by consistency”. By restricting the form of the traces, we show that global correctness in our system can be verified incrementally, taking advantage of the well-known size-change principle, which leads to an efficient implementation of proof search. Our CycleQ tool, accessible as a GHC plugin, shows promising results on a number of standard benchmarks.

Thu 16 Jun

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

10:40 - 12:00
AnalysisPLDI at Toucan +12h
Chair(s): Xiaokang Qiu Purdue University, USA
10:40
20m
Talk
CycleQ: an efficient basis for cyclic equational reasoning
PLDI
Eddie Jones University of Bristol, C.-H. Luke Ong University of Oxford, Steven Ramsay University of Bristol
DOI
11:00
20m
Talk
Finding the Dwarf: Recovering Precise Types from WebAssembly Binaries
PLDI
Daniel Lehmann University of Stuttgart, Michael Pradel University of Stuttgart
DOI Pre-print
11:20
20m
Talk
Abstract Interpretation Repair
PLDI
Roberto Bruni University of Pisa, Roberto Giacobazzi University of Verona, Roberta Gori University of Pisa, Francesco Ranzato University of Padova
DOI Pre-print
11:40
20m
Talk
Differential Cost Analysis with Simultaneous Potentials and Anti-potentials
PLDI
Đorđe Žikelić IST Austria, Pauline Bolignano Amazon, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon, Franco Raimondi Amazon & Middlesex University
DOI Pre-print
22:40 - 00:00
AnalysisPLDI at Toucan
22:40
20m
Talk
CycleQ: an efficient basis for cyclic equational reasoning
PLDI
Eddie Jones University of Bristol, C.-H. Luke Ong University of Oxford, Steven Ramsay University of Bristol
DOI
23:00
20m
Talk
Finding the Dwarf: Recovering Precise Types from WebAssembly Binaries
PLDI
Daniel Lehmann University of Stuttgart, Michael Pradel University of Stuttgart
DOI Pre-print
23:20
20m
Talk
Abstract Interpretation Repair
PLDI
Roberto Bruni University of Pisa, Roberto Giacobazzi University of Verona, Roberta Gori University of Pisa, Francesco Ranzato University of Padova
DOI Pre-print
23:40
20m
Talk
Differential Cost Analysis with Simultaneous Potentials and Anti-potentials
PLDI
Đorđe Žikelić IST Austria, Pauline Bolignano Amazon, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon, Franco Raimondi Amazon & Middlesex University
DOI Pre-print