SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025
Fri 17 Oct 2025 14:15 - 14:30 at Orchid Small - Semantics Chair(s): Hakjoo Oh

This paper proposes a mechanized formal semantics for \emph{dataflow} circuits: rather than following a static schedule predetermined at generation time, the execution of the components in a circuit is constrained solely by the availability of their input data.

We model circuit components as abstract computing units, asynchronously connected with each other through unidirectional, unbounded FIFO. In contrast to Kahn’s classic, denotational semantic framework, our semantics is operational. It intends to reflect Dennis’ dataflow paradigm with firing, while still formalizing the observable behaviors of circuits as channels histories.

The components we handle are either stateless or stateful, and may be non-deterministic. We formalize sufficient conditions to achieve the determinacy of circuits executions: all possible schedules of such circuits lead to a unique observable behavior. We provide two equivalent views for circuits. The first one is a direct and natural representation as graphs of components. The second is a core, structured term calculus, which enables constructing and reasoning about circuits in a inductive way. We prove that both representations are semantically equivalent.

We conduct our formalization within the Coq proof assistant. We experimentally validate its relevance by applying our general semantic framework to dataflow circuits generated with Dynamatic, a recent HLS tool exploiting dataflow circuits to generate dynamically scheduled, elastic circuits.

Fri 17 Oct

Displayed time zone: Perth change

13:45 - 15:30
SemanticsOOPSLA at Orchid Small
Chair(s): Hakjoo Oh Korea University
13:45
15m
Talk
A complete formal semantics of eBPF instruction set architecture for Solana
OOPSLA
Shenghao Yuan Zhejiang University, Zhuoruo Zhang Zhejiang University, Jiayi Lu Zhejiang University, David Sanan Singapore Institute of Technology, Rui Chang Zhejiang University, Yongwang Zhao Zhejiang University
14:00
15m
Talk
Adequacy for Algebraic Effects Revisited
OOPSLA
Alex Kavvos University of Bristol
14:15
15m
Talk
A Mechanized Semantics for Dataflow Circuits
OOPSLA
Tony Law Univ Rennes, Inria, CNRS, IRISA, Delphine Demange Univ Rennes, Inria, CNRS, IRISA, Sandrine Blazy University of Rennes
14:30
15m
Talk
Dynamic Wind for Effect Handlers
OOPSLA
David Voigt University of Tübingen, Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen
Pre-print
14:45
15m
Talk
React-tRace: A Semantics for Understanding React Hooks
OOPSLA
Jay Lee Seoul National University, Joongwon Ahn Seoul National University, Kwangkeun Yi Seoul National University
Link to publication DOI
15:00
15m
Talk
Semantics of Sets of Programs
OOPSLA
Jinwoo Kim University of Wisconsin-Madison; Seoul National University, Shaan Nagy University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison, Loris D'Antoni University of California at San Diego
15:15
15m
Talk
Zero-Overhead Lexical Effect Handlers
OOPSLA
Cong Ma University of Waterloo, Zhaoyi Ge University of Waterloo, Max Jung University of Waterloo, Yizhou Zhang University of Waterloo