Publications (6)
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…
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…
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…
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…
Crux, a Precise Verifier for Rust and Other Languages
Stuart Pernsteiner, Iavor S. Diatchki, Robert Dockins +6
We present Crux, a cross-language verification tool for Rust and C/LLVM. Crux targets bounded, intricate pieces of code that are difficult for humans to get right: for example, cry…
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…