Contract Lenses: Reasoning about Bidirectional Programs via CalculationJFP First Paper
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 SepDisplayed 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 18mTalk | 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 18mTalk | Level-p-complexity of Boolean functions using thinning, memoization, and polynomialsJFP First Paper JFP First Papers DOI | ||
16:06 18mTalk | 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 18mTalk | 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 |