Time Aware Compilation Verified: A Category-Theoretic Approach in Rocq

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.