The Stanford Software Research Lunch is a weekly event on Thursday where students and researchers present their latest work to peers. Talks are open to anybody, but regular attendees are expected to give a presentation on their work.  Members of the Computer Forum are especially welcome.

Mailing list: software-research-lunch@lists.stanford.edu (subscribe via mailman)

Calendar: ical

Format: The lunch is held every week during fall, winter and spring quarter. The first week of every quarter is an organizational lunch where people can sign up to give a talk. If you'd like to give a talk, please contact Rohan Yadav.

Past quarters: Winter 2026, Fall 2025, Spring 2025, Winter 2025, Fall 2024, Spring 2024, Winter 2024, Fall 2023, Spring 2023, Winter 2023, Fall 2022, Winter 2021, Fall 2020, Winter 2020, Fall 2019, Spring 2019, Winter 2019, Fall 2018, Spring 2018, Winter 2018, Fall 2017, Spring 2017, Winter 2017, Fall 2016.

Ordering Food: For suggestions for those ordering food for the lunch, see here.

4/2: From Operational Semantics to Tradeable Coupons

Time: Thursday, April 2, 2026, 12 noon - 1pm
Location: CoDa E401

Speaker: Yuhan Deng

Abstract: Building on our work on Fixpoint, starting from a set of operational semantics, we explore how to materialize facts, both operational ones (e.g. that a handle evaluates to a certain result), and equivalence ones (e.g. two handles are indistinguishable from the perspective of user programs) as coupons that can be combined and reasoned about via a set of trading rules. The goal is to allow untrusted, user-provided scheduler to make scheduling and optimizing decisions, as long as they can achieve the desired coupon.
To show that the set of trades is sound, we model the observational equivalence between handles/objects in Isabelle. We begin with a base coinductive relation, extend it with lemmas that capture nontrivial properties given our modeling of the system, and lift it into an equivalence relation through closure. We then define an inductive relation describing valid coupon trades and prove that it is sound with respect to this equivalence. Finally, we implement the coupon trading component as a WebAssembly program, and show that it faithfully implements the trades using the Isabelle mechanization of Wasm reference interpreter.

Food:

4/9: Fully-Automatic Type Inference for Borrows with Lifetimes

Time: Thursday, April 9, 2026, 12 noon - 1pm
Location: CoDa E401

Speaker: Benjamin Driscoll

Abstract: We present a new pure functional language and type system with borrows with lifetimes, and a corresponding fully-automatic type inference procedure. Inference provides users the performance benefits of borrows with lifetimes without requiring user annotation. If the user's program cannot be typed, inference inserts a handful of reference count operations so that it can be typed. We provide a heap semantics for our borrowing language and prove a soundness theorem, guaranteeing that well-typed programs do not violate memory safety. We implement our memory management strategy as part of the Morphic language stack and compare it to Perceus, a state-of-the-art reference-counting technique based on linear type inference. We find that our system is able to eliminate almost all reference count operations across a range of programs, reducing reference count increments by 75–100% on all benchmarks with reference count increments under the baseline. As a result, we achieve a 1.48× geomean speedup overall on all benchmarks.

Food:

4/16: Heuristic Approaches to Hard Combinatorial Optimization on In-Memory Computing Architectures

Time: Thursday, April 16, 2026, 12 noon - 1pm
Location: CoDa E401

Speaker: Alexander Stepanov

Abstract: This talk presents work from the Large-Scale Integrated Photonics team at Hewlett Packard Labs, where the broader research explores in-memory computing accelerators for hard optimization problems like Boolean Satisfiability (SAT). At the core of this work are stochastic local search heuristics, extended to natively handle hybrid XOR-CNF problem structures that arise in domains such as cryptography and AI planning. To overcome the challenge of local minima, we employ parallel tempering with a radical exchange mechanism that enables efficient exploration of complex solution landscapes. These approaches are developed and benchmarked using CountryCrab, a GPU-based hardware simulator that evaluates accelerator performance before hardware fabrication.

Food:

4/23: TBD

Time: Thursday, April 23, 2026, 12 noon - 1pm
Location: CoDa E401

Speaker: TBD

Abstract: TBD

Food:

4/30: TBD

Time: Thursday, April 30, 2026, 12 noon - 1pm
Location: CoDa E401

Speaker: TBD

Abstract: TBD

Food:

5/7: TBD

Time: Thursday, May 7, 2026, 12 noon - 1pm
Location: CoDa E401

Speaker: TBD

Abstract: TBD

Food:

5/14: TBD

Time: Thursday, May 14, 2026, 12 noon - 1pm
Location: CoDa E401

Speaker: TBD

Abstract: TBD

Food:

5/21: TBD

Time: Thursday, May 21, 2026, 12 noon - 1pm
Location: CoDa E401

Speaker: TBD

Abstract: TBD

Food:

5/28: TBD

Time: Thursday, May 28, 2026, 12 noon - 1pm
Location: CoDa E401

Speaker: TBD

Abstract: TBD

Food:

6/4: TBD (NOTE: Location is CoDa W401)

Time: Thursday, June 4, 2026, 12 noon - 1pm
Location: CoDa E401

Speaker: TBD

Abstract: TBD

Food: