Appeared at ICFP 2023

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

timelyembedding ofdiscreteinformation in temporallycontinuoussignals. 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

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.thentrying to prove their correctness, acompositionally correctmethodology 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 thelinearityof circuit timing (over a suitable semiring), thus enabling practical, modular, and fully verified timing analysis as linear maps over higher-dimensional time intervals.

- Paper (PDF)
- Talk slides (PDF)
- Video to appear.

```
@inproceedings{Elliott-2023-timely-computation,
title = {Timely Computation},
author = {Conal Elliott},
year = {2023},
month = {aug},
booktitle = {Proceedings of the ACM on Programming Languages},
number = {ICFP},
volume = {7},
articleno = {219},
numpages = {25},
url = {http://conal.net/papers/timely-computation/}
}
```