Showing 1–12 of 12 results for author: Kuper, L

Freer Arrows and Why You Need Them in Haskell

Authors: Grant VanDomelen, Gan Shen, Lindsey Kuper, Yao Li

Abstract: Freer monads are a useful structure commonly used in various domains due to their expressiveness. However, a known issue with freer monads is that they are not amenable to static analysis. This paper explores freer arrows, a relatively expressive structure that is amenable to static analysis. We propose several variants of freer arrows. We conduct a case study on choreographic programming to demon… ▽ More Freer monads are a useful structure commonly used in various domains due to their expressiveness. However, a known issue with freer monads is that they are not amenable to static analysis. This paper explores freer arrows, a relatively expressive structure that is amenable to static analysis. We propose several variants of freer arrows. We conduct a case study on choreographic programming to demonstrate the usefulness of freer arrows in Haskell. △ Less

Submitted 13 June, 2025; originally announced June 2025.

Comments: In submission to the Haskell Symposium 2025

CRDT Emulation, Simulation, and Representation Independence

Authors: Nathan Liittschwager, Jonathan Castello, Stelios Tsampas, Lindsey Kuper

Abstract: Conflict-free replicated data types (CRDTs) are distributed data structures designed for fault tolerance and high availability. CRDTs can be taxonomized into state-based CRDTs, in which replicas apply updates locally and periodically broadcast their local state to other replicas, and operation-based (op-based) CRDTs, in which every state-updating operation is individually broadcast and applied at… ▽ More Conflict-free replicated data types (CRDTs) are distributed data structures designed for fault tolerance and high availability. CRDTs can be taxonomized into state-based CRDTs, in which replicas apply updates locally and periodically broadcast their local state to other replicas, and operation-based (op-based) CRDTs, in which every state-updating operation is individually broadcast and applied at each replica. In the literature, state-based and op-based CRDTs are considered equivalent due to the existence of algorithms that transform one kind of CRDT into the other. In particular, verification techniques and results for one kind of CRDT are often said to be applicable to the other kind, thanks to this equivalence. However, what it means for state-based and op-based CRDTs to emulate each other has never been made fully precise. In particular, emulation is nontrivial since state-based and op-based CRDTs place different requirements on the behavior of the underlying network with regard to both the causal ordering of message delivery, and the granularity of the messages themselves. In this paper, we specify and formalize CRDT emulation in terms of simulation by modeling CRDTs and their interactions with the network as formal transition systems. We show that emulation can be understood as weak simulations between the transition systems of the original and emulating CRDT systems, thus closing a gap in the CRDT literature. We precisely characterize which properties of CRDT systems are preserved by our weak simulations, and therefore which properties can be said to be applicable to state-based CRDTs as long as they are applicable to op-based CRDTs and vice versa. Finally, we leverage our emulation results to obtain a general representation independence result for CRDTs: intuitively, clients of a CRDT cannot tell whether they are interacting with a state-based or op-based CRDT in particular. △ Less

Submitted 7 April, 2025; originally announced April 2025.

Efficient, Portable, Census-Polymorphic Choreographic Programming

Authors: Mako Bates, Shun Kashiwa, Syed Jafri, Gan Shen, Lindsey Kuper, Joseph P. Near

Abstract: Choreographic programming (CP) is a paradigm for implementing distributed systems that uses a single global program to define the actions and interactions of all participants. Library-level CP implementations, like HasChor, integrate well with mainstream programming languages but have several limitations: Their conditionals require extra communication; they require specific host-language features… ▽ More Choreographic programming (CP) is a paradigm for implementing distributed systems that uses a single global program to define the actions and interactions of all participants. Library-level CP implementations, like HasChor, integrate well with mainstream programming languages but have several limitations: Their conditionals require extra communication; they require specific host-language features (e.g., monads); and they lack support for programming patterns that are essential for implementing realistic distributed applications. We make three contributions to library-level CP to specifically address these challenges. First, we propose and formalize conclaves and multiply-located values, which enable efficient conditionals in library-level CP without redundant communication. Second, we propose end-point projection as dependency injection, a design pattern that enables library-level CP in host languages without support for monads. Third, we propose census polymorphism, a technique for abstracting over the number of participants in a choreography. We demonstrate these contributions via implementations in Haskell, Rust, and TypeScript. △ Less

Submitted 23 April, 2025; v1 submitted 2 December, 2024; originally announced December 2024.

Comments: Presenting at PLDI25

Toward Verified Library-Level Choreographic Programming with Algebraic Effects

Authors: Gan Shen, Lindsey Kuper

Abstract: Choreographic programming (CP) is a paradigm for programming distributed applications as single, unified programs, called choreographies, that are then compiled to node-local programs via endpoint projection (EPP). Recently, library-level CP frameworks have emerged, in which choreographies and EPP are expressed as constructs in an existing host language. So far, however, library-level CP lacks a s… ▽ More Choreographic programming (CP) is a paradigm for programming distributed applications as single, unified programs, called choreographies, that are then compiled to node-local programs via endpoint projection (EPP). Recently, library-level CP frameworks have emerged, in which choreographies and EPP are expressed as constructs in an existing host language. So far, however, library-level CP lacks a solid theoretical foundation. In this paper, we propose modeling library-level CP using algebraic effects, an abstraction that generalizes the approach taken by existing CP libraries. Algebraic effects let us define choreographies as computations with user-defined effects and EPP as location-specific effect handlers. Algebraic effects also lend themselves to reasoning about correctness properties, such as soundness and completeness of EPP. We present a prototype of a library-level CP framework based on algebraic effects, implemented in the Agda proof assistant, and discuss our ongoing work on leveraging the algebraic-effects-based approach to prove the correctness of our library-level CP implementation. △ Less

Submitted 8 July, 2024; originally announced July 2024.

Comments: Talk proposal for Choreographic Programming 2024

Portable, Efficient, and Practical Library-Level Choreographic Programming

Authors: Shun Kashiwa, Gan Shen, Soroush Zare, Lindsey Kuper

Abstract: Choreographic programming (CP) is an emerging paradigm for programming distributed applications that run on multiple nodes. In CP, the programmer writes one program, called a choreography, that is then transformed to individual programs for each node via a compilation step called endpoint projection (EPP). While CP languages have existed for over a decade, library-level CP -- in which choreographi… ▽ More Choreographic programming (CP) is an emerging paradigm for programming distributed applications that run on multiple nodes. In CP, the programmer writes one program, called a choreography, that is then transformed to individual programs for each node via a compilation step called endpoint projection (EPP). While CP languages have existed for over a decade, library-level CP -- in which choreographies are expressed as programs in an existing host language, and choreographic language constructs and EPP are provided entirely by a host-language library -- is in its infancy. Library-level CP has great potential, but existing implementations have portability, efficiency, and practicality drawbacks that hinder its adoption. In this paper, we aim to advance the state of the art of library-level CP with two novel techniques for choreographic library design and implementation: endpoint projection as dependency injection (EPP-as-DI), and choreographic enclaves. EPP-as-DI is a language-agnostic technique for implementing EPP at the library level. Unlike existing library-level approaches, EPP-as-DI asks little from the host language -- support for higher-order functions is all that is required -- making it usable in a wide variety of host languages. Choreographic enclaves are a language feature that lets the programmer define sub-choreographies within a larger choreography. Within an enclave, "knowledge of choice" is propagated only among the enclave's participants, enabling the seamless use of the host language's conditional constructs while addressing the efficiency limitations of existing library-level CP implementations. We implement EPP-as-DI and choreographic enclaves in ChoRus, the first CP library for the Rust programming language. Our case studies and benchmarks demonstrate that the usability and performance of ChoRus compares favorably to traditional distributed programming in Rust. △ Less

Submitted 19 November, 2023; originally announced November 2023.

An Exceptional Actor System (Functional Pearl)

Authors: Patrick Redmond, Lindsey Kuper

Abstract: The Glasgow Haskell Compiler is known for its feature-laden runtime system (RTS), which includes lightweight threads, asynchronous exceptions, and a slew of other features. Their combination is powerful enough that a programmer may complete the same task in many different ways -- some more advisable than others. We present a user-accessible actor framework hidden in plain sight within the RTS an… ▽ More The Glasgow Haskell Compiler is known for its feature-laden runtime system (RTS), which includes lightweight threads, asynchronous exceptions, and a slew of other features. Their combination is powerful enough that a programmer may complete the same task in many different ways -- some more advisable than others. We present a user-accessible actor framework hidden in plain sight within the RTS and demonstrate it on a classic example from the distributed systems literature. We then extend both the framework and example to the realm of dynamic types. Finally, we raise questions about how RTS features intersect and possibly subsume one another, and suggest that GHC can guide good practice by constraining the use of some features. △ Less

Submitted 20 July, 2023; originally announced July 2023.

Comments: To appear at Haskell Symposium 2023

Inductive diagrams for causal reasoning

Authors: Jonathan Castello, Patrick Redmond, Lindsey Kuper

Abstract: The Lamport diagram is a pervasive and intuitive tool for informal reasoning about "happens-before" relationships in a concurrent system. However, traditional axiomatic formalizations of Lamport diagrams can be painful to work with in a mechanized setting like Agda. We propose an alternative, inductive formalization -- the causal separation diagram (CSD) -- that takes inspiration from string diagr… ▽ More The Lamport diagram is a pervasive and intuitive tool for informal reasoning about "happens-before" relationships in a concurrent system. However, traditional axiomatic formalizations of Lamport diagrams can be painful to work with in a mechanized setting like Agda. We propose an alternative, inductive formalization -- the causal separation diagram (CSD) -- that takes inspiration from string diagrams and concurrent separation logic, but enjoys a graphical syntax similar to Lamport diagrams. Critically, CSDs are based on the idea that causal relationships between events are witnessed by the paths that information follows between them. To that end, we model happens-before as a dependent type of paths between events. The inductive formulation of CSDs enables their interpretation into a variety of semantic domains. We demonstrate the interpretability of CSDs with a case study on properties of logical clocks, widely-used mechanisms for reifying causal relationships as data. We carry out this study by implementing a series of interpreters for CSDs, culminating in a generic proof of Lamport's clock condition that is parametric in a choice of clock. We instantiate this proof on Lamport's scalar clock, on Mattern's vector clock, and on the matrix clocks of Raynal et al. and of Wuu and Bernstein, yielding verified implementations of each. The CSD formalism and our case study are mechanized in the Agda proof assistant. △ Less

Submitted 14 May, 2024; v1 submitted 19 July, 2023; originally announced July 2023.

Comments: This revision is as published in PACMPL through OOPSLA, but with [authorversion] set. Compared to the previous version, the introduction has been almost entirely rewritten

Journal ref: Proc. ACM Program. Lang. 8, OOPSLA1, Article 113 (April 2024), 26 pages

HasChor: Functional Choreographic Programming for All (Functional Pearl)

Authors: Gan Shen, Shun Kashiwa, Lindsey Kuper

Abstract: Choreographic programming is an emerging paradigm for programming distributed systems. In choreographic programming, the programmer describes the behavior of the entire system as a single, unified program -- a choreography -- which is then compiled to individual programs that run on each node, via a compilation step called endpoint projection. We present a new model for functional choreographic pr… ▽ More Choreographic programming is an emerging paradigm for programming distributed systems. In choreographic programming, the programmer describes the behavior of the entire system as a single, unified program -- a choreography -- which is then compiled to individual programs that run on each node, via a compilation step called endpoint projection. We present a new model for functional choreographic programming where choreographies are expressed as computations in a monad. Our model supports cutting-edge choreographic programming features that enable modularity and code reuse: in particular, it supports higher-order choreographies, in which a choreography may be passed as an argument to another choreography, and location-polymorphic choreographies, in which a choreography can abstract over nodes. Our model is implemented in a Haskell library, HasChor, which lets programmers write choreographic programs while using the rich Haskell ecosystem at no cost, bringing choreographic programming within reach of everyday Haskellers. Moreover, thanks to Haskell's abstractions, the implementation of the HasChor library itself is concise and understandable, boiling down endpoint projection to its short and simple essence. △ Less

Submitted 19 July, 2023; v1 submitted 1 March, 2023; originally announced March 2023.

Verified Causal Broadcast with Liquid Haskell

Authors: Patrick Redmond, Gan Shen, Niki Vazou, Lindsey Kuper

Abstract: Protocols to ensure that messages are delivered in causal order are a ubiquitous building block of distributed systems. For instance, distributed data storage systems can use causally ordered message delivery to ensure causal consistency, and CRDTs can rely on the existence of an underlying causally-ordered messaging layer to simplify their implementation. A causal delivery protocol ensures that w… ▽ More Protocols to ensure that messages are delivered in causal order are a ubiquitous building block of distributed systems. For instance, distributed data storage systems can use causally ordered message delivery to ensure causal consistency, and CRDTs can rely on the existence of an underlying causally-ordered messaging layer to simplify their implementation. A causal delivery protocol ensures that when a message is delivered to a process, any causally preceding messages sent to the same process have already been delivered to it. While causal delivery protocols are widely used, verification of their correctness is less common, much less machine-checked proofs about executable implementations. We implemented a standard causal broadcast protocol in Haskell and used the Liquid Haskell solver-aided verification system to express and mechanically prove that messages will never be delivered to a process in an order that violates causality. We express this property using refinement types and prove that it holds of our implementation, taking advantage of Liquid Haskell's underlying SMT solver to automate parts of the proof and using its manual theorem-proving features for the rest. We then put our verified causal broadcast implementation to work as the foundation of a distributed key-value store. △ Less

Submitted 15 March, 2023; v1 submitted 29 June, 2022; originally announced June 2022.

Comments: Appeared at IFL 2022

Toward SMT-Based Refinement Types in Agda

Authors: Gan Shen, Lindsey Kuper

Abstract: Dependent types offer great versatility and power, but developing proofs with them can be tedious and requires considerable human guidance. We propose to integrate Satisfiability Modulo Theories (SMT)-based refinement types into the dependently-typed language Agda in an effort to ease some of the burden of programming with dependent types and combine the strengths of the two approaches to mechaniz… ▽ More Dependent types offer great versatility and power, but developing proofs with them can be tedious and requires considerable human guidance. We propose to integrate Satisfiability Modulo Theories (SMT)-based refinement types into the dependently-typed language Agda in an effort to ease some of the burden of programming with dependent types and combine the strengths of the two approaches to mechanized theorem proving. △ Less

Submitted 12 October, 2021; originally announced October 2021.

Comments: Accepted for publication at HATRA 2021

Toward Hole-Driven Development with Liquid Haskell

Authors: Patrick Redmond, Gan Shen, Lindsey Kuper

Abstract: Liquid Haskell is an extension to the Haskell programming language that adds support for refinement types: data types augmented with SMT-decidable logical predicates that refine the set of values that can inhabit a type. Furthermore, Liquid Haskell's support for refinement reflection enables the use of Haskell for general-purpose mechanized theorem proving. A growing list of large-scale mechanized… ▽ More Liquid Haskell is an extension to the Haskell programming language that adds support for refinement types: data types augmented with SMT-decidable logical predicates that refine the set of values that can inhabit a type. Furthermore, Liquid Haskell's support for refinement reflection enables the use of Haskell for general-purpose mechanized theorem proving. A growing list of large-scale mechanized proof developments in Liquid Haskell take advantage of this capability. Adding theorem-proving capabilities to a "legacy" language like Haskell lets programmers directly verify properties of real-world Haskell programs (taking advantage of the existing highly tuned compiler, run-time system, and libraries), just by writing Haskell. However, more established proof assistants like Agda and Coq offer far better support for interactive proof development and insight into the proof state (for instance, what subgoals still need to be proved to finish a partially-complete proof). In contrast, Liquid Haskell provides only coarse-grained feedback to the user -- either it reports a type error, or not -- unfortunately hindering its usability as a theorem prover. In this paper, we propose improving the usability of Liquid Haskell by extending it with support for Agda-style typed holes and interactive editing commands that take advantage of them. In Agda, typed holes allow programmers to indicate unfinished parts of a proof, and incrementally complete the proof in a dialogue with the compiler. While GHC Haskell already has its own Agda-inspired support for typed holes, we posit that typed holes would be especially powerful and useful if combined with Liquid Haskell's refinement types and SMT automation. We discuss how typed holes might work in Liquid Haskell, and we consider possible implementation approaches and next steps. △ Less

Submitted 9 October, 2021; originally announced October 2021.

Comments: Accepted for publication at HATRA 2021

Toward Scalable Verification for Safety-Critical Deep Networks

Authors: Lindsey Kuper, Guy Katz, Justin Gottschlich, Kyle Julian, Clark Barrett, Mykel Kochenderfer

Abstract: The increasing use of deep neural networks for safety-critical applications, such as autonomous driving and flight control, raises concerns about their safety and reliability. Formal verification can address these concerns by guaranteeing that a deep learning system operates as intended, but the state of the art is limited to small systems. In this work-in-progress report we give an overview of ou… ▽ More The increasing use of deep neural networks for safety-critical applications, such as autonomous driving and flight control, raises concerns about their safety and reliability. Formal verification can address these concerns by guaranteeing that a deep learning system operates as intended, but the state of the art is limited to small systems. In this work-in-progress report we give an overview of our work on mitigating this difficulty, by pursuing two complementary directions: devising scalable verification techniques, and identifying design choices that result in deep learning systems that are more amenable to verification. △ Less

Submitted 2 February, 2018; v1 submitted 18 January, 2018; originally announced January 2018.

Comments: Accepted for presentation at SysML 2018