Timely Computation
summary
Defines a digital circuit as an analog circuit used in a disciplined way and formalizes that notion in Agda formalization, embedding discrete meanings into continuous signals via per-bit stability intervals (stability = value holds over an interval). Timing combines three operations — Minkowski sum (convolution), intersection, and offsets — forming a semiring so that timing is linear over a semiring and composes as linear maps represented by matrix timing analysis. Works through a full-adder example and shows compositional correctness via functorial homomorphisms.
AI-written summary · about
chapters (7)
- 0:00The nature of computation
- 2:20Defining digital circuits
- 5:56Correctness in computing
- 8:56Compositional frameworks
- 14:40Timing and stability
- 20:48Analyzing circuit timing
- 26:40Q&A on hardware systems
related talks
01h 07mAn introduction to synthetic guarded domain theory with applications to probabilistic(…)
30mComputation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations
20mA Graded Modal Type Theory for Pulse Schedules
25mCubical Synthetic Homotopy Theory
23mSmooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs(…)
17mAn Algebra of Sequential Decision Problems
30mSymbolic Execution of Hadamard-Toffoli Quantum Circuits
51mOn constant T-depth circuits