Time: Fridays, noon - 1:05pm (PT)
Location: The Internet / The LSD Lab (Engineering 2, Room 398)
Organizers: Sabrina Reis, Achilles Benetopoulos, and Lindsey Kuper
The Languages, Systems, and Data Seminar meets weekly to discuss interesting topics in the areas of programming languages, systems, databases, formal methods, security, software engineering, verification, architecture, and beyond. Our goal is to encourage interactions and discussions between students, researchers, and faculty with interests in these areas. The seminar is open to everyone interested. Participating UCSC students should register for the 2-credit course CSE 280O (let the organizers know if you’re an undergrad and need a permission code).
For fall 2026, we will continue to host the LSD Seminar in a hybrid fashion. Anyone can attend on Zoom, and local folks can gather in person in the lab. Speakers can join either in person or on Zoom, whichever is convenient.
Talks will be advertised on the ucsc-lsd-seminar-announce (for anyone) and lsd-group (for UCSC-affiliated people) mailing lists.
| Date | Speaker | Title |
|---|---|---|
| September 25 | Tim Goodwin | SOSP Practice Talk and New Student Welcome |
| October 2 | Yan Tong | Ironwright: A Rusty Bridge from Bounded Model Checking to Full Verification |
| October 9 | Gavin Gray | A Design Space Exploration of Async/Await |
| October 16 | Ashley Samuelson | Choreographic Programming: Abstractions for Concurrent Dynamism and Modularity |
| October 23 | N/A | Social Hour |
| October 30 | Clara “Clarise” Ceerla | Mocha: A Motion-Based Choreographic Language |
| November 6 | Esteban Ramos | Constraints, Explanations, and Search: Using Propagator Networks to Modularize Non-Deterministic Components |
| November 13 | Ashton Wiersdorf | TBD |
| November 20 | Keith Allen | ChorMPI: Choreographies for HPC |
| November 27 | No Speaker | Thanksgiving Holiday |
September 25
The first half hour will consist of a practice talk for SOSP given by Tim Goodwin. The second half hour will be a social with a focus on welcoming new students to the LSD lab.
Speaker: Tim Goodwin
Title: Testing Custom Control Planes Without The Cluster
Abstract: Modern cloud infrastructure is increasingly managed by software. On platforms like Kubernetes, the control plane maintains desired system state through controllers: software components that continuously monitor cluster resources and reconcile them toward a declared specification. This pattern has proven effective, and a thriving ecosystem of projects now compose controllers into custom control planes (CCPs) to automate tasks such as managing application delivery, scaling infrastructure dynamically, and composing cloud provider APIs into higher-level abstractions. The correctness of a CCP, however, depends on how its constituent controllers interact at run time. Bugs arise from implicit assumptions about these interactions that do not hold under all possible executions. As such, finding them requires enumerating the space of possible executions and searching it systematically, which is infeasible in a live cluster environment. In this talk, I will present Kamera, a system for testing CCPs that uses partial simulation to execute the code of multiple interacting controllers against a lightweight model of the Kubernetes runtime. Thus far, Kamera has found 31 new bugs in five popular CCP projects and achieves a 1,781× speedup over existing cluster-based controller testing approaches.
Bio: Tim is a fifth-year PhD student at UC Santa Cruz co-advised by Andi Quinn and Lindsey Kuper.
October 2
Speaker: Yan Tong
Title: Ironwright: A Rusty Bridge from Bounded Model Checking to Full Verification (HATRA Talk)
Abstract: Despite decades of progress on tools for formal verification of distributed systems, it is still hard for verification engineers to close the gap from bounded model checking to full verification. Verification tools that do bridge that gap stop short of producing practically deployable code. We propose Ironwright, a verification framework that addresses these gaps through a unified Rust-based workflow. Developers model and implement distributed systems in a Rust-based shallowly embedded DSL, validate them via automated bounded model checking for rapid iteration, and then “intract” formal specifications from Rust to the Lean proof assistant for rigorous verification. The framework will let developers obtain both verified correctness guarantees and deployable code from the same program.
Bio: Yan is a fourth-year PhD student advised by Prof. Lindsey Kuper. His research focuses on distributed systems verification.
October 9
Speaker: Gavin Gray
Title: A Design Space Exploration of Async/Await
Abstract: Many modern programming languages include some form of asynchronous programming. In particular, a growing number now have what we call straight-line asynchrony: attempts to provide asynchronous functions that look similar to synchronous functions, thereby enabling asynchrony without introducing complex control. These languages often share construct names like async and await, which suggests that they have deep semantic similarities. Yet, a close examination reveals that these languages are quite different along several dimensions, often subtly. These differences have real semantic consequences: similar-looking programs can exhibit divergent behavior, confusing developers and language designers alike.
In this talk I will present our design space exploration of straight-line asynchrony with async/await. We will dissect several existing languages and show how no two of them agree as a whole on design decisions that affect the presence and ordering of effects. I will articulate a design space with nine dimensions covering the full lifecycle of an asynchronous computation, covering questions such as: What precise guarantees does a language give upon calling an asynchronous function? What happens at the end of a task’s life? How can a task handle be cancelled? We will explore these questions through concrete examples, informal design discussion, and a formal semantics.
Bio: Gavin Gray is a PhD student at Brown University advised by Will Crichton and Shriram Krishnamurthi. Gavin works on material to improve the experience of learning and using advanced languages. He currently is focusing on constructs for advanced control flow such as coroutines, effects, continuations, and async/await. Gavin works at the intersection of HCI, applied cognitive science, and programming languages, doing what he refers to as: the human factors of PL design.
October 16
Speaker: Ashley Samuelson
Title: Choreographic Programming: Abstractions for Concurrent Dynamism and Modularity
Abstract: Choreographic programming is an emerging paradigm for writing concurrent programs where developers write a single centralized program that compiles to an individual program for each node. Choreographies provide a high-level abstraction for modeling concurrent systems that both yields intuitive interfaces for programmers and enables correct-by-construction guarantees. However, there are still gaps between the features of existing choreographic languages and the features which are needed and expected by modern systems and their programmers. In this talk, I will present my prior and ongoing work to identify areas in which these disparities arise and address these gaps by designing new choreographic languages and type systems.
Note: This job talk is geared towards a general computer science audience and does not require deep knowledge of programming language theory or concurrency to comprehend. Undergraduates are encouraged to attend!
Bio: Ashley is a Ph.D. candidate in Computer Science at UW—Madison, where she is advised by Ethan Cecchetti, and also frequently collaborates with Andrew K. Hirsch at the University at Buffalo, SUNY. Her research is in the area of programming language and type system design, specifically focusing on choreographic programming, a programming paradigm for deadlock-free message-passing concurrency.
October 23
Social Hour
October 30
Speaker: Clara “Clarise” Ceerla
Title: Mocha: A Motion-Based Choreographic Language
Abstract: Computer systems with multiple parts that execute at the same time– concurrent systems– can be described both informally, with gesture, and formally, with rigorous models such as process calculi and choreographies, and with Lamport diagrams, which can be both informal and formal. They can also be described locally, from the point-of-view of the parts of the system (processes), or globally, as if observed by an outsider. We propose a way to bridge these representations: Mocha gestural programming. The Mocha programming language, a gestural programming language, bridges local, informal gestures and local, formal process calculi. A choreographic synthesizer bridges these process calculi with global, formal choreographies when possible. Finally, Mocha’s Lamport diagram generator bridges choreographies with global Lamport diagrams.
Bio: Clarise is a first-year Master’s student advised by Dr. Lindsey Kuper at UCSC. His research currently focuses on stretching PL methodology to unusual subjects, such as gestural programming or TTRPGs.
November 6
Speaker: Esteban Ramos
Title: Constraints, Explanations, and Search: Using Propagator Networks to Modularize Non-Deterministic Components
Abstract: Contemporary application design is increasingly influenced by the prevalence of probabilistic components. Black box machine learning models output predictions that are taken as actionable information by both software and human systems. Generative AI has become a commonly relied upon reasoning oracle for human interaction and as a flexible decision making agent for software to respond to novel scenarios. While the motivations for their implementation are not ill-founded, this trend has introduced a novel kind of non-determinism into our software applications. The inherently probabilistic nature of black box models leaves our software systems increasingly opaque, with notions of correct behavior measured in likelihoods and probabilities. The difficulties in gaining visibility into their behavior leaves us not only with a lack of guarantees over software behavior but also a lack of explanations, with attribution for abnormal executions left as a matter of study instead of as an observable component of the application’s design.
This talk will argue that there must be an intentional accounting of probabilistic non-determinism when designing applications that leverage black box models. We will explore the use of the Propagator Networks programming model as a viable framework to build systems with probabilistic components, and cover its support for constraints, explanations, and search. This will be followed by a presentation of two software vignettes demonstrating the use of propagator networks in applications with black box models; a medical diagnosis assistance tool and an autonomous vehicle driving system.
Bio: Esteban Ramos is a 6th year PhD Student in CSE advised by Dr. Leilani Gilpin. Their current work focuses on evaluating propagator networks as a viable programming model to provide greater reliability in non-deterministic systems.
November 13
Speaker: Ashton Wiersdorf
Title: TBD
November 20
Speaker: Keith Allen
Title: ChorMPI: Choreographies for HPC
Bio: TBD
November 27
Speaker: No Speaker
No seminar due to Thanksgiving holiday.