一句话：在Agda中形式化数字电路，将离散信息适时嵌入连续时间信号，并支持组合式正确的计时分析。
论文追问“数字电路是什么”，针对实际物理电路本质上是模拟的这一问题，给出简单非形式定义，并在证明助手Agda中以构造类型论进行形式化。其核心是把离散信息适时嵌入时间连续信号；该嵌入可泛化地从单信号扩展到多信号，从布尔逻辑门扩展到任意复杂的串行与并行组合，从而构成计算电路。与先构造电路再证明正确性不同，方法在每一步同时维护规约、实现、时序与正确性证明，并用统一的代数词汇与同态联系各层面。形式化证明后，作者应用若干关键变换，揭示电路时序在合适半环上的线性性，从而把计时分析化为高维时间区间上的线性映射，实现实用、模块化且完全验证的分析。全文强调规约的简单性与通用性。
This paper addresses the question “what is a digital circuit?” in relation to the fundamentally analog nature of actual (physical) circuits. A simple informal definition is given and then formalized in the proof assistant Agda. At the heart of this definition is the timely embedding of discrete information in temporally continuous signals. Once this embedding is defined (in constructive logic, i.e., type theory), it is extended in a generic fashion from one signal to many and from simple boolean operations (logic gates) to arbitrarily sophisticated sequential and parallel compositions, i.e., to computational circuits. Rather than constructing circuits and then trying to prove their correctness, a compositionally correct methodology maintains specification, implementation, timing, and correctness proofs at every step. Compositionality of each aspect and of their combination is supported by a single, shared algebraic vocabulary and related by homomorphisms. After formally defining and proving these notions, a few key transformations are applied to reveal the linearity of circuit timing (over a suitable semiring), thus enabling practical, modular, and fully verified timing analysis as linear maps over higher-dimensional time intervals. An emphasis throughout the paper is simplicity and generality of specification, minimizing circuit-specific definitions and proofs while highlighting a broadly applicable methodology of scalable, compositionally correct engineering through simple denotations and homomorphisms.