Dan R. Ghica ; George Kaye ; David Sprunger - A Complete Theory of Sequential Digital Circuits: Denotational, Operational and Algebraic Semantics

lmcs:15508 - Logical Methods in Computer Science, June 29, 2026, Volume 22, Issue 2 - https://doi.org/10.46298/lmcs-22(2:34)2026
A Complete Theory of Sequential Digital Circuits: Denotational, Operational and Algebraic SemanticsArticle

Authors: Dan R. Ghica ; George Kaye ; David Sprunger

Digital circuits, despite having been studied for nearly a century and used at scale for about half that time, have until recently evaded a fully compositional theoretical in which arbitrary circuits may be freely composed together without consulting their internals. Recent work remedied this theoretical shortcoming by showing how digital circuits can be presented compositionally as morphisms in a freely generated symmetric traced category. However, this was done informally; in this paper we refine and expand the previous work in several ways, culminating in the presentation of three sound and complete semantics for digital circuits: denotational, operational and algebraic. For the denotational semantics, we establish a correspondence between stream functions with certain properties and circuits constructed syntactically. For the operational semantics, we present the reductions required to model how a circuit processes a value, including the addition of a new reduction for eliminating non-delay-guarded feedback; this leads to an adequate notion of observational equivalence for digital circuits. Finally, we define a new family of equations for translating circuits into bisimilar circuits of a 'normal form', leading to a complete algebraic semantics for sequential circuits.


Volume: Volume 22, Issue 2
Published on: June 29, 2026
Accepted on: May 2, 2026
Submitted on: April 15, 2025
Keywords: Logic in Computer Science, Programming Languages, Category Theory

Consultation statistics

This page has been seen 318 times.
This article's PDF has been downloaded 69 times.