ICFP 2024
Mon 2 - Sat 7 September 2024 Milan, Italy
Wed 4 Sep 2024 16:24 - 16:42 at Green 1-2-3 - Verification and Cost Analysis Chair(s): Clément Pit-Claudel

Bidirectional transformations (BXs) are a mechanism for maintaining consistency between multiple representations of related data. The lens framework, which usually constructs BXs from lens combinators, has become the mainstream approach to BX programming because of its modularity and correctness by construction. However, the involved bidirectional behaviors of lenses make the equational reasoning and optimization of them much harder than unidirectional programs. We propose a novel approach to deriving efficient lenses from clear specifications via program calculation, a correct-by-construction approach to reasoning about functional programs by algebraic laws. To support bidirectional program calculation, we propose contract lenses, which extend conventional lenses with a pair of predicates to enable safe and modular composition of partial lenses. We define several contract-lens combinators capturing common computation patterns including fold,filter,map, and scan, and develop several bidirectional calculation laws to reason about and optimize contract lenses. We demonstrate the effectiveness of our new calculation framework based on contract lenses with nontrivial examples.

Wed 4 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:30 - 16:42
Verification and Cost AnalysisJFP First Papers / ICFP Papers and Events at Green 1-2-3
Chair(s): Clément Pit-Claudel EPFL
15:30
18m
Talk
Story of Your Lazy Function’s Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs
ICFP Papers and Events
Li-yao Xia Unaffiliated, Laura Israel Portland State University, Maite Kramarz University of Toronto, Nicholas Coltharp Portland State University, Koen Claessen Chalmers University of Technology, Stephanie Weirich University of Pennsylvania, Yao Li Portland State University
DOI Pre-print
15:48
18m
Talk
Level-p-complexity of Boolean functions using thinning, memoization, and polynomialsJFP First Paper
JFP First Papers
Julia Jansson , Patrik Jansson Chalmers University of Technology and University of Gothenbrug
DOI
16:06
18m
Talk
CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs
ICFP Papers and Events
Cole Kurashige University of California at San Diego, Ruyi Ji Peking University, Aditya Giridharan University of California at San Diego, Mark Barbone University of California at San Diego, Daniel Noor Technion, Shachar Itzhaky Technion, Ranjit Jhala University of California at San Diego, Nadia Polikarpova University of California at San Diego
DOI
16:24
18m
Talk
Contract Lenses: Reasoning about Bidirectional Programs via CalculationJFP First Paper
JFP First Papers
Hanliang Zhang University of Bristol, UK, Wenhao Tang University of Edinburgh, Ruifeng Xie Peking University, Meng Wang University of Bristol, Zhenjiang Hu Peking University
DOI