21 citations · 57 across the 12 of their papers we have counts for
12 papers
Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern
Patrick Redmond, Jonathan Castello, José Manuel Calderón Trilla +1
The Entity-Component-System (ECS) software design pattern, long used in game development, encourages a clean separation of identity (entities), data properties (components), and co…
Freer Arrows and Why You Need Them in Haskell
Grant VanDomelen, Gan Shen, Lindsey Kuper +1
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 a…
Efficient, Portable, Census-Polymorphic Choreographic Programming
Mako Bates, Shun Kashiwa, Syed Jafri +3
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. Libr…
Toward Verified Library-Level Choreographic Programming with Algebraic Effects
Gan Shen, Lindsey Kuper
Choreographic programming (CP) is a paradigm for programming distributed applications as single, unified programs, called choreographies, that are then compiled to node-local progr…
Portable, Efficient, and Practical Library-Level Choreographic Programming
Shun Kashiwa, Gan Shen, Soroush Zare +1
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 chore…
An Exceptional Actor System (Functional Pearl)
Patrick Redmond, Lindsey Kuper
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 c…
Inductive diagrams for causal reasoning
Jonathan Castello, Patrick Redmond, Lindsey Kuper
The Lamport diagram is a pervasive and intuitive tool for informal reasoning about "happens-before" relationships in a concurrent system. However, traditional axiomatic formalizati…
HasChor: Functional Choreographic Programming for All (Functional Pearl)
Gan Shen, Shun Kashiwa, Lindsey Kuper
Choreographic programming is an emerging paradigm for programming distributed systems. In choreographic programming, the programmer describes the behavior of the entire system as a…
Verified Causal Broadcast with Liquid Haskell
Patrick Redmond, Gan Shen, Niki Vazou +1
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 causa…
Toward SMT-Based Refinement Types in Agda
Gan Shen, Lindsey Kuper
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 M…
Toward Hole-Driven Development with Liquid Haskell
Patrick Redmond, Gan Shen, Lindsey Kuper
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 th…
Toward Scalable Verification for Safety-Critical Deep Networks
Lindsey Kuper, Guy Katz, Justin Gottschlich +3
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. Form…