Showing 1–20 of 20 results for author: Zdancewic, S

Functional Meaning for Parallel Streaming

Authors: Nick Rioux, Steve Zdancewic

Abstract: Nondeterminism introduced by race conditions and message reorderings makes parallel and distributed programming hard. Nevertheless, promising approaches such as LVars and CRDTs address this problem by introducing a partial order structure on shared state that describes how the state evolves over time. Monotone programs that respect the order are deterministic. Datalog-inspired languages incorporat… ▽ More Nondeterminism introduced by race conditions and message reorderings makes parallel and distributed programming hard. Nevertheless, promising approaches such as LVars and CRDTs address this problem by introducing a partial order structure on shared state that describes how the state evolves over time. Monotone programs that respect the order are deterministic. Datalog-inspired languages incorporate this idea of monotonicity in a first-class way but they are not general-purpose. We would like parallel and distributed languages to be as natural to use as any functional language, without sacrificing expressivity, and with a formal basis of study as appealing as the lambda calculus. This paper presents $λ_\vee$, a core language for deterministic parallelism that embodies the ideas above. In $λ_\vee$, values may increase over time according to a streaming order and all computations are monotone with respect to that order. The streaming order coincides with the approximation order found in Scott semantics and so unifies the foundations of functional programming with the foundations of deterministic distributed computation. The resulting lambda calculus has a computationally adequate model rooted in domain theory. It integrates the compositionality and power of abstraction characteristic of functional programming with the declarative nature of Datalog. This version of the paper includes extended exposition and appendices with proofs. △ Less

Submitted 3 April, 2025; originally announced April 2025.

Comments: Extended version of paper to appear in PLDI 2025

Structural temporal logic for mechanized program verification

Authors: Eleftherios Ioannidis, Yannick Zakowski, Steve Zdancewic, Sebastian Angel

Abstract: Mechanized verification of liveness properties for infinite programs with effects and nondeterminism is challenging. Existing temporal reasoning frameworks operate at the level of models such as traces and automata. Reasoning happens at a very low-level, requiring complex nested (co-)inductive proof techniques and familiarity with proof assistant mechanics (e.g., the guardedness checker). Further,… ▽ More Mechanized verification of liveness properties for infinite programs with effects and nondeterminism is challenging. Existing temporal reasoning frameworks operate at the level of models such as traces and automata. Reasoning happens at a very low-level, requiring complex nested (co-)inductive proof techniques and familiarity with proof assistant mechanics (e.g., the guardedness checker). Further, reasoning at the level of models instead of program constructs creates a verification gap that loses the benefits of modularity and composition enjoyed by structural program logics such as Hoare Logic. To address this verification gap, and the lack of compositional proof techniques for temporal specifications, we propose Ticl, a new structural temporal logic. Using ticl, we encode complex (co-)inductive proof techniques as structural lemmas and focus our reasoning on variants and invariants. We show that it is possible to perform compositional proofs of general temporal properties in a proof assistant, while working at a high level of abstraction. We demonstrate the benefits of Ticl by giving mechanized proofs of safety and liveness properties for programs with scheduling, concurrent shared memory, and distributed consensus, demonstrating a low proof-to-code ratio. △ Less

Submitted 7 April, 2025; v1 submitted 18 October, 2024; originally announced October 2024.

Opportunistically Parallel Lambda Calculus. Or, Lambda: The Ultimate LLM Scripting Language

Authors: Stephen Mell, Konstantinos Kallas, Steve Zdancewic, Osbert Bastani

Abstract: Scripting languages are widely used to compose external calls, such as foreign functions that perform expensive computations, remote APIs, and more recently, machine learning systems such as large language models (LLMs). The execution time of scripts is often dominated by waiting for these external calls, and large speedups can be achieved via parallelization and streaming. However, doing this man… ▽ More Scripting languages are widely used to compose external calls, such as foreign functions that perform expensive computations, remote APIs, and more recently, machine learning systems such as large language models (LLMs). The execution time of scripts is often dominated by waiting for these external calls, and large speedups can be achieved via parallelization and streaming. However, doing this manually is challenging, even for expert programmers. To address this, we propose a novel opportunistic evaluation strategy for scripting languages based on a core lambda calculus that automatically executes external calls in parallel, as early as possible. We prove that our approach is confluent, ensuring that it preserves the programmer's original intent, and that our approach eventually executes every external call. We implement this approach in a framework called EPIC, embedded in Python. We demonstrate its versatility and performance on several applications drawn from the LLM literature, including Tree-of-Throughts and tool use. Our experiments show that opportunistic evaluation improves total running time (up to $6.2\times$) and latency (up to $12.7\times$) compared to several state-of-the-art baselines, while performing very close (between $1.3\%$ and $18.5\%$ running time overhead) to hand-tuned manually optimized parallel Rust implementations. △ Less

Submitted 19 January, 2025; v1 submitted 18 May, 2024; originally announced May 2024.

A Two-Phase Infinite/Finite Low-Level Memory Model

Authors: Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski, Steve Zdancewic

Abstract: This paper provides a novel approach to reconciling complex low-level memory model features, such as pointer--integer casts, with desired refinements that are needed to justify the correctness of program transformations. The idea is to use a "two-phased" memory model, one with and unbounded memory and corresponding unbounded integer type, and one with a finite memory; the connection between the tw… ▽ More This paper provides a novel approach to reconciling complex low-level memory model features, such as pointer--integer casts, with desired refinements that are needed to justify the correctness of program transformations. The idea is to use a "two-phased" memory model, one with and unbounded memory and corresponding unbounded integer type, and one with a finite memory; the connection between the two levels is made explicit by our notion of refinement that handles out-of-memory behaviors. This approach allows for more optimizations to be performed and establishes a clear boundary between the idealized semantics of a program and the implementation of that program on finite hardware. To demonstrate the utility of this idea in practice, we instantiate the two-phase memory model in the context of Zakowski et al.'s VIR semantics, yielding infinite and finite memory models of LLVM IR, including low-level features like undef and bitcast. Both the infinite and finite models, which act as specifications, can provably be refined to executable reference interpreters. The semantics justify optimizations, such as dead-alloca-elimination, that were previously impossible or difficult to prove correct. △ Less

Submitted 24 April, 2024; originally announced April 2024.

ACM Class: D.3.1

Journal ref: 2024

Syntax Monads for the Working Formal Metatheorist

Authors: Lawrence Dunn, Val Tannen, Steve Zdancewic

Abstract: Formally verifying the properties of formal systems using a proof assistant requires justifying numerous minor lemmas about capture-avoiding substitution. Despite work on category-theoretic accounts of syntax and variable binding, raw, first-order representations of syntax, the kind considered by many practitioners and compiler frontends, have received relatively little attention. Therefore applic… ▽ More Formally verifying the properties of formal systems using a proof assistant requires justifying numerous minor lemmas about capture-avoiding substitution. Despite work on category-theoretic accounts of syntax and variable binding, raw, first-order representations of syntax, the kind considered by many practitioners and compiler frontends, have received relatively little attention. Therefore applications miss out on the benefits of category theory, most notably the promise of reusing formalized infrastructural lemmas between implementations of different systems. Our Coq framework Tealeaves provides libraries of reusable infrastructure for a raw, locally nameless representation and can be extended to other representations in a modular fashion. In this paper we give a string-diagrammatic account of decorated traversable monads (DTMs), the key abstraction implemented by Tealeaves. We define DTMs as monoids of structured endofunctors before proving a representation theorem a la Kleisli, yielding a recursion combinator for finitary tree-like datatypes. △ Less

Submitted 14 December, 2023; originally announced December 2023.

Comments: In Proceedings ACT 2023, arXiv:2312.08138

Journal ref: EPTCS 397, 2023, pp. 98-117

Ideograph: A Language for Expressing and Manipulating Structured Data

Authors: Stephen Mell, Osbert Bastani, Steve Zdancewic

Abstract: We introduce Ideograph, a language for expressing and manipulating structured data. Its types describe kinds of structures, such as natural numbers, lists, multisets, binary trees, syntax trees with variable binding, directed multigraphs, and relational databases. Fully normalized terms of a type correspond exactly to members of the structure, analogous to a Church-encoding. Moreover, definable op… ▽ More We introduce Ideograph, a language for expressing and manipulating structured data. Its types describe kinds of structures, such as natural numbers, lists, multisets, binary trees, syntax trees with variable binding, directed multigraphs, and relational databases. Fully normalized terms of a type correspond exactly to members of the structure, analogous to a Church-encoding. Moreover, definable operations over these structures are guaranteed to respect the structures' equivalences. In this paper, we give the syntax and semantics of the non-polymorphic subset of Ideograph, and we demonstrate how it can represent and manipulate several interesting structures. △ Less

Submitted 28 March, 2023; originally announced March 2023.

Comments: In Proceedings TERMGRAPH 2022, arXiv:2303.14219

Journal ref: EPTCS 377, 2023, pp. 65-84

Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq

Authors: Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic

Abstract: This paper introduces Choice Trees (ctrees), a monad for modeling nondeterministic, recursive, and impure programs in Coq. Inspired by Xia et al.'s itrees, this novel data structure embeds computations into coinductive trees with three kind of nodes: external events, and two variants of nondeterministic branching. This apparent redundancy allows us to provide shallow embedding of denotational mode… ▽ More This paper introduces Choice Trees (ctrees), a monad for modeling nondeterministic, recursive, and impure programs in Coq. Inspired by Xia et al.'s itrees, this novel data structure embeds computations into coinductive trees with three kind of nodes: external events, and two variants of nondeterministic branching. This apparent redundancy allows us to provide shallow embedding of denotational models with internal choice in the style of ccs, while recovering an inductive LTS view of the computation. CTrees inherit a vast collection of bisimulation and refinement tools, with respect to which we establish a rich equational theory. We connect ctrees to the itrees infrastructure by showing how a monad morphism embedding the former into the latter permits to use ctrees to implement nondeterministic effects. We demonstrate the utility of ctrees by using them to model concurrency semantics in two case studies: ccs and cooperative multithreading. △ Less

Submitted 13 November, 2022; originally announced November 2022.

Counterfactual Explanations for Natural Language Interfaces

Authors: George Tolkachev, Stephen Mell, Steve Zdancewic, Osbert Bastani

Abstract: A key challenge facing natural language interfaces is enabling users to understand the capabilities of the underlying system. We propose a novel approach for generating explanations of a natural language interface based on semantic parsing. We focus on counterfactual explanations, which are post-hoc explanations that describe to the user how they could have minimally modified their utterance to ac… ▽ More A key challenge facing natural language interfaces is enabling users to understand the capabilities of the underlying system. We propose a novel approach for generating explanations of a natural language interface based on semantic parsing. We focus on counterfactual explanations, which are post-hoc explanations that describe to the user how they could have minimally modified their utterance to achieve their desired goal. In particular, the user provides an utterance along with a demonstration of their desired goal; then, our algorithm synthesizes a paraphrase of their utterance that is guaranteed to achieve their goal. In two user studies, we demonstrate that our approach substantially improves user performance, and that it generates explanations that more closely match the user's intent compared to two ablations. △ Less

Submitted 27 April, 2022; originally announced April 2022.

Comments: 6 pages, 1 figure, 1 algorithm, 1 table. To be published in Association for Computational Linguistics 2022 conference

Model-Based Testing of Networked Applications

Authors: Yishuai Li, Benjamin C. Pierce, Steve Zdancewic

Abstract: We present a principled automatic testing framework for application-layer protocols. The key innovation is a domain-specific embedded language for writing nondeterministic models of the behavior of networked servers. These models are defined within the Coq interactive theorem prover, supporting a smooth transition from testing to formal verification. Given a server model, we show how to automati… ▽ More We present a principled automatic testing framework for application-layer protocols. The key innovation is a domain-specific embedded language for writing nondeterministic models of the behavior of networked servers. These models are defined within the Coq interactive theorem prover, supporting a smooth transition from testing to formal verification. Given a server model, we show how to automatically derive a tester that probes the server for unexpected behaviors. We address the uncertainties caused by both the server's internal choices and the network delaying messages nondeterministically. The derived tester accepts server implementations whose possible behaviors are a subset of those allowed by the nondeterministic model. We demonstrate the effectiveness of this framework by using it to specify and test a fragment of the HTTP/1.1 protocol, showing that the automatically derived tester can capture RFC violations in buggy server implementations, including the latest versions of Apache and Nginx. △ Less

Submitted 2 July, 2021; v1 submitted 30 January, 2021; originally announced February 2021.

Comments: 11 pages, 15 figures

ACM Class: D.2.5; F.3.1

Journal ref: Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2021). Association for Computing Machinery, New York, NY, USA, 529--539

An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction

Authors: Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic

Abstract: Coinductive reasoning about infinitary structures such as streams is widely applicable. However, practical frameworks for developing coinductive proofs and finding reasoning principles that help structure such proofs remain a challenge, especially in the context of machine-checked formalization. This paper gives a novel presentation of an equational theory for reasoning about structures up to we… ▽ More Coinductive reasoning about infinitary structures such as streams is widely applicable. However, practical frameworks for developing coinductive proofs and finding reasoning principles that help structure such proofs remain a challenge, especially in the context of machine-checked formalization. This paper gives a novel presentation of an equational theory for reasoning about structures up to weak bisimulation. The theory is both compositional, making it suitable for defining general-purpose lemmas, and also incremental, meaning that the bisimulation can be created interactively. To prove the theory's soundness, this paper also introduces generalized parameterized coinduction, which addresses expressivity problems of earlier works and provides a practical framework for coinductive reasoning. The paper presents the resulting equational theory for streams, but the technique applies to other structures too. All of the results in this paper have been proved in Coq, and the generalized parameterized coinduction framework is available as a Coq library. △ Less

Submitted 8 January, 2020; originally announced January 2020.

Comments: To be published in CPP 2020

Interaction Trees: Representing Recursive and Impure Programs in Coq

Authors: Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic

Abstract: "Interaction trees" (ITrees) are a general-purpose data structure for representing the behaviors of recursive programs that interact with their environments. A coinductive variant of "free monads," ITrees are built out of uninterpreted events and their continuations. They support compositional construction of interpreters from "event handlers", which give meaning to events by defining their semant… ▽ More "Interaction trees" (ITrees) are a general-purpose data structure for representing the behaviors of recursive programs that interact with their environments. A coinductive variant of "free monads," ITrees are built out of uninterpreted events and their continuations. They support compositional construction of interpreters from "event handlers", which give meaning to events by defining their semantics as monadic actions. ITrees are expressive enough to represent impure and potentially nonterminating, mutually recursive computations, while admitting a rich equational theory of equivalence up to weak bisimulation. In contrast to other approaches such as relationally specified operational semantics, ITrees are executable via code extraction, making them suitable for debugging, testing, and implementing software artifacts that are amenable to formal verification. We have implemented ITrees and their associated theory as a Coq library, mechanizing classic domain- and category-theoretic results about program semantics, iteration, monadic structures, and equational reasoning. Although the internals of the library rely heavily on coinductive proofs, the interface hides these details so that clients can use and reason about ITrees without explicit use of Coq's coinduction tactics. To showcase the utility of our theory, we prove the termination-sensitive correctness of a compiler from a simple imperative source language to an assembly-like target whose meanings are given in an ITree-based denotational semantics. Unlike previous results using operational techniques, our bisimulation proof follows straightforwardly by structural induction and elementary rewriting via an equational theory of combinators for control-flow graphs. △ Less

Submitted 14 November, 2019; v1 submitted 31 May, 2019; originally announced June 2019.

Comments: 28 pages, 4 pages references, published at POPL 2020

A HoTT Quantum Equational Theory (Extended Version)

Authors: Jennifer Paykin, Steve Zdancewic

Abstract: This paper presents an equational theory for the QRAM model of quantum computation, formulated as an embedded language inside of homotopy type theory. The embedded language approach is highly expressive, and reflects the style of state-of-the art quantum languages like Quipper and QWIRE. The embedding takes advantage of features of homotopy type theory to encode unitary transformations as higher i… ▽ More This paper presents an equational theory for the QRAM model of quantum computation, formulated as an embedded language inside of homotopy type theory. The embedded language approach is highly expressive, and reflects the style of state-of-the art quantum languages like Quipper and QWIRE. The embedding takes advantage of features of homotopy type theory to encode unitary transformations as higher inductive paths, simplifying the presentation of an equational theory. We prove that this equational theory is sound and complete with respect to established models of quantum computation. △ Less

Submitted 8 April, 2019; originally announced April 2019.

ReQWIRE: Reasoning about Reversible Quantum Circuits

Authors: Robert Rand, Jennifer Paykin, Dong-Ho Lee, Steve Zdancewic

Abstract: Common quantum algorithms make heavy use of ancillae: scratch qubits that are initialized at some state and later returned to that state and discarded. Existing quantum circuit languages let programmers assert that a qubit has been returned to the |0> state before it is discarded, allowing for a range of optimizations. However, existing languages do not provide the tools to verify these assertions… ▽ More Common quantum algorithms make heavy use of ancillae: scratch qubits that are initialized at some state and later returned to that state and discarded. Existing quantum circuit languages let programmers assert that a qubit has been returned to the |0> state before it is discarded, allowing for a range of optimizations. However, existing languages do not provide the tools to verify these assertions, introducing a potential source of errors. In this paper we present methods for verifying that ancillae are discarded in the desired state, and use these methods to implement a verified compiler from classical functions to quantum oracles. △ Less

Submitted 29 January, 2019; originally announced January 2019.

Comments: In Proceedings QPL 2018, arXiv:1901.09476

ACM Class: D.2.4; F.3.1

Journal ref: EPTCS 287, 2019, pp. 299-312

From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server

Authors: Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic

Abstract: We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable… ▽ More We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward "one client at a time" style, with the CompCert semantics of the C program. The variability introduced by low-level buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement. △ Less

Submitted 28 November, 2018; originally announced November 2018.

Comments: 13 pages + references

Journal ref: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '19), January 14--15, 2019, Cascais, Portugal

Synthesizing Symmetric Lenses

Authors: Anders Miltner, Solomon Maina, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic

Abstract: Lenses are programs that can be run both "front to back" and "back to front," allowing updates to either their source or their target data to be transferred in both directions. Lenses have been extensively studied, extended, and applied. Recent work has demonstrated how techniques from type-directed program synthesis can be used to efficiently synthesize a simple class of lenses---bijective lenses… ▽ More Lenses are programs that can be run both "front to back" and "back to front," allowing updates to either their source or their target data to be transferred in both directions. Lenses have been extensively studied, extended, and applied. Recent work has demonstrated how techniques from type-directed program synthesis can be used to efficiently synthesize a simple class of lenses---bijective lenses over string data---given a pair of types (regular expressions) and examples. We extend this synthesis algorithm to a broader class of lenses, called simple symmetric lenses, including all bijective lenses, all of the popular category of "asymmetric" lenses, and a subset of the "symmetric lenses" proposed by Hofmann et al. Intuitively, simple symmetric lenses allow some information to be present on one side but not the other and vice versa. They are of independent theoretical interest, being the largest class of symmetric lenses that do not use persistent internal state. Synthesizing simple symmetric lenses is more challenging than synthesizing bijective lenses: Since some of the information on each side can be "disconnected" from the other side, there will typically be many lenses that agree with a given example. To guide the search process, we use stochastic regular expressions and information theory to estimate the amount of information propagated by a candidate lens, preferring lenses that propagate more information, as well as user annotations marking parts of the source and target formats as either irrelevant or essential. We describe an implementation of simple symmetric lenses and our synthesis procedure as extensions to the Boomerang language. We evaluate its performance on 48 benchmark examples drawn from Flash Fill, Augeas, and the bidirectional programming literature. Our implementation can synthesize each of these lenses in under 30 seconds. △ Less

Submitted 25 June, 2019; v1 submitted 26 October, 2018; originally announced October 2018.

Comments: ICFP 2019

Structural Operational Semantics for Control Flow Graph Machines

Authors: Dmitri Garbuzov, William Mansky, Christine Rizkallah, Steve Zdancewic

Abstract: Compilers use control flow graph (CFG) representations of low-level programs because they are suited to program analysis and optimizations. However, formalizing the behavior and metatheory of CFG programs is non-trivial: CFG programs don't compose well, their semantics depends on auxiliary state, and, as a consequence, they do not enjoy a simple equational theory that can be used for reasoning abo… ▽ More Compilers use control flow graph (CFG) representations of low-level programs because they are suited to program analysis and optimizations. However, formalizing the behavior and metatheory of CFG programs is non-trivial: CFG programs don't compose well, their semantics depends on auxiliary state, and, as a consequence, they do not enjoy a simple equational theory that can be used for reasoning about the correctness of program transformations. Lambda-calculus-based intermediate representations, in contrast, have well-understood operational semantics and metatheory, including rich equational theories, all of which makes them amenable to formal verification. This paper establishes a tight equivalence between (a variant of) Levy's call-by-push-value (CBPV) calculus and a control flow graph machine whose instructions are in static single assignment (SSA) form. The correspondence is made precise via a series of abstract machines that align the transitions of the structural operational semantics of the CBPV language with the computation steps of the SSA form. The target machine, which is derived from the CBPV language, accurately captures the execution model of control flow graphs, including direct jumps, mutually recursive code blocks, and multi-argument function calls, and the closure-free subset is similar to the SSA intermediate representations found in modern compilers such as LLVM and GCC. The definitions of all the language/abstract machine semantics and the theorems relating them are fully verified in Coq. △ Less

Submitted 14 May, 2018; originally announced May 2018.

QWIRE Practice: Formal Verification of Quantum Circuits in Coq

Authors: Robert Rand, Jennifer Paykin, Steve Zdancewic

Abstract: We describe an embedding of the QWIRE quantum circuit language in the Coq proof assistant. This allows programmers to write quantum circuits using high-level abstractions and to prove properties of those circuits using Coq's theorem proving features. The implementation uses higher-order abstract syntax to represent variable binding and provides a type-checking algorithm for linear wire types, ensu… ▽ More We describe an embedding of the QWIRE quantum circuit language in the Coq proof assistant. This allows programmers to write quantum circuits using high-level abstractions and to prove properties of those circuits using Coq's theorem proving features. The implementation uses higher-order abstract syntax to represent variable binding and provides a type-checking algorithm for linear wire types, ensuring that quantum circuits are well-formed. We formalize a denotational semantics that interprets QWIRE circuits as superoperators on density matrices, and prove the correctness of some simple quantum programs. △ Less

Submitted 1 March, 2018; originally announced March 2018.

Comments: In Proceedings QPL 2017, arXiv:1802.09737

ACM Class: D.2.4; F.3.1

Journal ref: EPTCS 266, 2018, pp. 119-132

Synthesizing Bijective Lenses

Authors: Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic

Abstract: Bidirectional transformations between different data representations occur frequently in modern software systems. They appear as serializers and deserializers, as database views and view updaters, and more. Manually building bidirectional transformations---by writing two separate functions that are intended to be inverses---is tedious and error prone. A better approach is to use a domain-specific… ▽ More Bidirectional transformations between different data representations occur frequently in modern software systems. They appear as serializers and deserializers, as database views and view updaters, and more. Manually building bidirectional transformations---by writing two separate functions that are intended to be inverses---is tedious and error prone. A better approach is to use a domain-specific language in which both directions can be written as a single expression. However, these domain-specific languages can be difficult to program in, requiring programmers to manage fiddly details while working in a complex type system. To solve this, we present Optician, a tool for type-directed synthesis of bijective string transformers. The inputs to Optician are two ordinary regular expressions representing two data formats and a few concrete examples for disambiguation. The output is a well-typed program in Boomerang (a bidirectional language based on the theory of lenses). The main technical challenge involves navigating the vast program search space efficiently enough. Unlike most prior work on type-directed synthesis, our system operates in the context of a language with a rich equivalence relation on types (the theory of regular expressions). We synthesize terms of a equivalent language and convert those generated terms into our lens language. We prove the correctness of our synthesis algorithm. We also demonstrate empirically that our new language changes the synthesis problem from one that admits intractable solutions to one that admits highly efficient solutions. We evaluate Optician on a benchmark suite of 39 examples including both microbenchmarks and realistic examples derived from other data management systems including Flash Fill, a tool for synthesizing string transformations in spreadsheets, and Augeas, a tool for bidirectional processing of Linux system configuration files. △ Less

Submitted 9 October, 2017; originally announced October 2017.

Comments: 127 Pages, Extended Version with Appendix

A Linear/Producer/Consumer Model of Classical Linear Logic

Authors: Jennifer Paykin, Steve Zdancewic

Abstract: This paper defines a new proof- and category-theoretic framework for classical linear logic that separates reasoning into one linear regime and two persistent regimes corresponding to ! and ?. The resulting linear/producer/consumer (LPC) logic puts the three classes of propositions on the same semantic footing, following Benton's linear/non-linear formulation of intuitionistic linear logic. Semant… ▽ More This paper defines a new proof- and category-theoretic framework for classical linear logic that separates reasoning into one linear regime and two persistent regimes corresponding to ! and ?. The resulting linear/producer/consumer (LPC) logic puts the three classes of propositions on the same semantic footing, following Benton's linear/non-linear formulation of intuitionistic linear logic. Semantically, LPC corresponds to a system of three categories connected by adjunctions reflecting the linear/producer/consumer structure. The paper's metatheoretic results include admissibility theorems for the cut and duality rules, and a translation of the LPC logic into category theory. The work also presents several concrete instances of the LPC model. △ Less

Submitted 16 February, 2015; originally announced February 2015.

Comments: In Proceedings LINEARITY 2014, arXiv:1502.04419

Journal ref: EPTCS 176, 2015, pp. 9-23

Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi

Authors: Benoît Valiron, Steve Zdancewic

Abstract: In this paper we use finite vector spaces (finite dimension, over finite fields) as a non-standard computational model of linear logic. We first define a simple, finite PCF-like lambda-calculus with booleans, and then we discuss two finite models, one based on finite sets and the other on finite vector spaces. The first model is shown to be fully complete with respect to the operational semantics… ▽ More In this paper we use finite vector spaces (finite dimension, over finite fields) as a non-standard computational model of linear logic. We first define a simple, finite PCF-like lambda-calculus with booleans, and then we discuss two finite models, one based on finite sets and the other on finite vector spaces. The first model is shown to be fully complete with respect to the operational semantics of the language. The second model is not complete, but we develop an algebraic extension of the finite lambda calculus that recovers completeness. The relationship between the two semantics is described, and several examples based on Church numerals are presented. △ Less

Submitted 5 June, 2014; originally announced June 2014.

Comments: Accepted at ICTAC 2014. The final publication will be available at link.springer.com

Journal ref: Proc. of ICTAC'14, in LNCS vol. 8687, pp 442-459 (2014)