(link to the article.) This is joint work with David Nowak.

Abstract

Certifying real-time guarantees for imperative programs is a critical challenge in embedded systems and cyber-physical applications. However, existing certified compilers lack the capability to accurately translate high-level timing abstractions into low-level executable code while preserving temporal semantics. This paper introduces a category-theoretic framework to model time-sensitive programs, leveraging monads and comonads to capture both the production and observation of temporal effects. Our methodology is formalized in the Rocq proof assistant, providing a foundation for the development of a certified compiler capable of preserving real-time constraints across compilation stages. By abstracting timing effects categorically, this work bridges the gap between theoretical program semantics and practical real-time certification, offering a principled path toward verified compilation for time-critical systems.

References

[1]: Benjamin Lion, David Nowak, Time Aware Compilation Verified: A Category-Theoretic Approach in Rocq https://dl.acm.org/doi/10.1145/3742875.3754693.

[2]: Benjamin Lion, Rocq implementation of the theory presented in the paper. n.d. “Bialgebraic semantics.” https://zenodo.org/records/16872463.