arXiv subjects

Ashley Samuelson

Publications and source records attributed to Ashley Samuelson.

3 recordsLinked to original sources

arXiv2026

Step in Tine: Forking Processes in Functional Choreographies

Traditional concurrent-programming techniques require programmers to painstakingly write programs for each participant in a concurrent system. Choreographic programming, in contrast, allows a programmer to write one centralized program and compile it to individual programs. This approach simplifies critical properties like deadlock freedom, but it complicates forking new processes, a core primitive in concurrent programming. This work addresses that gap with the choreographic fork calculus $\lambda{\pitchfork}$, the first functional choreographic language with process forking. $\lambda{\pitchfork}$ provides a deadlock-freedom guarantee while allowing programs to dynamically determine when to spawn new processes, what they will do, and who will communicate with them. In doing so, it supports practical applications like load balancers and parallel divide-and-conquer.

cs.PL↗

arXiv2025

zkStruDul: Programming zkSNARKs with Structural Duality

Non-Interactive Zero Knowledge (NIZK) proofs, such as zkSNARKS, let one prove knowledge of private data without revealing it or interacting with a verifier. While existing tooling focuses on specifying the predicate to be proven, real-world applications optimize predicate definitions to minimize proof generation overhead, but must correspondingly transform predicate inputs. Implementing these two steps separately duplicates logic that must precisely match to avoid catastrophic security flaws. We address this shortcoming with zkStruDul, a language that unifies input transformations and predicate definitions into a single combined abstraction from which a compiler can project both procedures, eliminating duplicate code and problematic mismatches. zkStruDul provides a high-level abstraction to layer on top of existing NIZK technology and supports important features like recursive proofs. We provide a source-level semantics and prove its behavior is identical to the projected semantics, allowing straightforward standard reasoning.

cs.PL↗

arXiv2025

Choreographic Quick Changes: First-Class Location (Set) Polymorphism

Choreographic programming is a promising new paradigm for programming concurrent systems where a developer writes a single centralized program that compiles to individual programs for each node. Existing choreographic languages, however, lack critical features integral to modern systems, like the ability of one node to dynamically compute who should perform a computation and send that decision to others. This work addresses this gap with $\lambda_{QC}$, the first typed choreographic language with \emph{first class process names} and polymorphism over both types and (sets of) locations. $\lambda_{QC}$ also improves expressive power over previous work by supporting algebraic and recursive data types as well as multiply-located values. We formalize and mechanically verify our results in Rocq, including the standard choreographic guarantee of deadlock freedom.

cs.PL↗