This program is tentative and subject to change.

Wed 26 Aug 2026 10:30 - 10:48 at IP126 Auditorium - Languages and DSLs Chair(s): Benjamin Delaware

Term rewriting systems are a common tool in automated reasoning and semantics of programming languages, and many practical applications require these systems to be convergent. While automated tools and theory exist to establish convergence, this paper is concerned with a practical method for testing it to quickly find useful counterexamples. Standard property-based testing approaches struggle here: exhaustively computing all normal forms is fundamentally flawed and too slow, while generating random normal forms makes counterexample minimization (shrinking) fragile due to dependencies on earlier generated test data. To solve this, we introduce a QuickCheck testing method based on generating and shrinking random execution traces. By checking if the first and last terms of a generated trace share the same deterministic normal form, we remove the data dependency between generators. This approach yields a property that efficiently finds counterexamples and enables fast, robust shrinking. We demonstrate the effectiveness of this method on various examples, ranging from group theory equations to distributed process calculus.

This program is tentative and subject to change.

Wed 26 Aug

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

10:30 - 12:00
Languages and DSLsICFP Papers at IP126 Auditorium
Chair(s): Benjamin Delaware Purdue University
10:30
18m
Talk
QuickChecking Convergence of Rewriting Systems (Functional Pearl)Remote
ICFP Papers
Koen Claessen Chalmers University of Technology
DOI
10:48
18m
Talk
Safety First: How to Safely Disregard Unsafe Behaviour in Compiler CalculationsRemote
ICFP Papers
Patrick Bahr IT University of Copenhagen
DOI Pre-print
11:06
18m
Talk
Assertions for Free: Transferring Invariants from Algorithm to Implementation Proofs (Functional Pearl)
ICFP Papers
Shushu Wu Shanghai Jiao Tong University, Chengxi Yang Shanghai Jiao Tong University, Xiwei Wu Shanghai Jiao Tong University, Qinxiang Cao Shanghai Jiao Tong University
DOI
11:24
18m
Talk
Package Managers à la Carte
ICFP Papers
Ryan Gibb University of Cambridge, Patrick Ferris University of Cambridge, UK, David Allsopp Jane Street, Thomas Gazagnaire Tarides, Anil Madhavapeddy University of Cambridge, UK
DOI
11:42
18m
Talk
Compositional Generator Equivalence
ICFP Papers
Anthony Vandikas University of Toronto, Kiarash Sotoudeh University of Toronto, Marsha Chechik University of Toronto
DOI
Hide past events