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

Benjamin Lion

Inria, University of Rennes,
Rennes, France

David Nowak

Univ. Lille, CNRS, Centrale Lille, UMR 9189 CRISTAL
F-59000 Lille, France

## 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.

## ACM Reference Format:

Benjamin Lion and David Nowak. 2025. Time Aware Compilation Verified: A Category-Theoretic Approach in Rocq. In *International Symposium on Formal Methods and Models for System Design (MEMOCODE '25), September 28-October 3, 2025, Taipei, Taiwan*. ACM, New York, NY, USA, 9 pages. https://doi.org/10.1145/3742875.3754693

## 1 Introduction

A compiler is a key component in applied and theoretical computer science, as this is the component that translates an input program into an output object executable by a machine. A compiler performs, in general, the operations in the following order: lexical analysis, preprocessing, parsing, semantic analysis, and finally generate optimized code. One important requirement is that each phase must preserve the semantics of the programming constructs. If the constraint holds, a programmer has the guarantee that the executable object corresponds to the behavior of the input program. A certified compiler therefore provably preserves the semantics of the input language, when translated to the output object. CompCert [10] is an example of such certified compiler, for the C language.

The C language is widely used to program embedded systems, as it gives more control over low level machine operations, such modulation of general purpose input/output (GPIO) and manipulation of register values. The intended meaning is no longer purely

functional, but aligns with the effect that a program has on its environment. Thus, a program that writes `pio(1, high)` intends to set the `pio` 1 to high. A program that has the instruction `delay 20 ms` intends to delay the execution by 20 ms. The semantic preservation theorem slightly changes: the meaning of an instruction depends on the effect that the instruction has at runtime.

For instance, on modern CPU, reading the Time Stamp Counter (TSC) is accessed by the `__rdtsc()` instruction, which returns the timing value from the TSC register that increases at the frequency of the processor clock. A `delay(n)` instruction would delay the operations for *n* unit of time. One of the challenge addressed in the paper is to give semantics for the two instructions such that a compiler could preserve the behavior during compilation.

```c
bits = [1,0,1,1,0,1,0];
gpio(1, 0);
t0 = __rdtsc();
i=0;
while(i < length(bits)){
    if((-rdtsc() - t0) > 10ms){
        t0 = __rdtsc();
        gpio(1, bits[i]);
        i++;
    }
};
```

<caption>**Listing 1: Time sensitive program**</caption>

To make the point more concrete, let us consider a simple program that generates a signal on one of its output, as shown in Listing 1. This signal could be used to communicate between two interconnected circuits. The intended observable output is therefore displayed in Figure 1, where the edge changes correspond to an interval of 10ms, as stated by the condition within the while loop. We take as simplifying assumption that the processor clock ticks at a constant rate, and do not consider energy saving mechanisms (such as down clocking).

<figure><img src="image_1.png" /><figcaption>**Figure 1: Semantics of the program in Listing 1**</figcaption></figure>

The main task of a certified compiler is therefore to provably verify that the executable object preserves the timing of the source program in Listing 1. At the operating system level, a major work of certification has been done in the seL4 project. However, “what seL4 cannot (yet) do, and no other OS can either, is to provide temporal isolation guarantees”. They continue with “we have not yet developed the formal framework for reasoning about timing

<footnote>Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s).

MEMOCODE '25, Taipei, Taiwan

© 2025 Copyright held by the owner/author(s).

ACM ISBN 979-8-4007-1994-3/2025/09

https://doi.org/10.1145/3742875.3754693</footnote>
guarantees on top of the Mixed Critical System model” to finish with “the world’s emerging cyberphysical systems need more”[23]. The approach in this paper is a first step towards certification of time guarantees on critical systems. To reach this point, it is necessary to extend the functional semantics of imperative programs with temporal effects. The object of this paper is to present a categorical framework to give a time-sensitive semantics for C-like language.

Our key insight is that time, like state or I/O, can be treated as an effect in the categorical sense [9], thus enabling the same rigorous reasoning about temporal compositionality that monads provide for other computational effects. This allows us to formulate compiler correctness not just as preservation of input/output behavior, but as preservation of temporal behavior across compilation stages. This approach is different from the ones taken in the analysis of the worst case execution time (WCET) of dedicated software [21], that lead to the successful company AbsInt. As the director and lead researcher said in a recent article [25], “the analysis of the worst-case execution time is not compositional: given a composition A;B, the execution time of instruction B may depend on the state of the architecture after execution of instruction A”. We propose to develop a compositional model of execution time at design level using similar advanced mathematics as those developed for compositional reasoning on memory manipulation.

The paper proceeds as follows: Section 2 introduces our categorical foundations, Section 3 develops the bialgebraic semantics for time-sensitive programs, Section 4 discusses compilation challenges, and Section 5 relates our approach to existing work.

All constructions are formalized in the Rocq proof assistant, providing machine-checked guarantees. While our current work focuses on a simplified imperative language and simplified computer architecture, the framework is designed to scale to realistic languages and architectures. This represents a crucial step toward verified compilation for cyber-physical systems, where timing guarantees are essential for safety-critical applications.

## 2 Category Theory for design and certification

Category theory provides a powerful framework for reasoning about program semantics, offering several key advantages.

It raises the level of abstraction. Indeed, by modelling programs and their behaviours using categorical structures (such as objects, morphisms, functors, and natural transformations) we move away from low-level implementation details and instead focus on high-level relationships and patterns. This abstraction helps in unifying different programming paradigms (functional, imperative, ...) under a common mathematical language.

It generalises theorems on abstract structures. Many results in programming language theory (e.g., recursion schemes, type system properties, and program equivalences) can be formulated and proven in the abstract setting of categories. Once a result is established categorically (e.g., the Yoneda Lemma, adjunctions, or monads) it can be instantiated across various concrete domains (such as sets, types, or processes) and reduces the need for redundant proofs.

It improves compositionality. A core principle of category theory is that complex systems can be built from simpler components via composition (e.g., morphism composition, monoidal products, or

pullbacks). In program semantics, this means that the meaning of a larger program can be derived systematically from the meanings of its subprograms, enabling modular reasoning and scalable verification.

By using category theory, we gain a unifying perspective that not only clarifies deep connections between disparate concepts but also provides robust tools for constructing and analysing programs in a principled way.

The need to formally capture the effects of program (such as state, I/O, exceptions, or non-determinism) on their environment led to the adoption of monads as a structuring tool for computational semantics. Eugenio Moggi's seminal work [15] demonstrated how monads in category theory provide a uniform way to extend the pure lambda calculus to model impure computations. By encapsulating side effects within a monadic type, programs remain composable while explicitly tracking their effects. This insight not only influenced theoretical foundations (e.g., denotational semantics) but also practical language design, as seen in Haskell's use of monads for effectful programming. It can then be used to reason formally on programs [1-3].

As the main application is about time, we first introduce an abstract model of time as a monoid.

**Definition 2.1 (Discrete Time as monoid).** A monoid is a triple $(T, +, 0)$ such that $+$ is a binary associative operation on $T$, for which $0 \in T$ is the identity.

An instance of a discrete time structure is the monoid $T_N = (\mathbb{N}, +, 0)$ where $\mathbb{N}$ is the set of natural numbers, $+$ is the addition on $\mathbb{N}$. We write $n - m$ as the number $x$ such that $m + x = n$ if $m \le n$, or $0$ otherwise.

Several categorical structures are of particular interest for our work, and we give their formal definitions hereafter. Each definition is followed by an example taken from [9], that captures computational and time sensitive aspects. All definitions and examples have been formalized in the Rocq proof assistant [11].

**Definition 2.2.** A monad on a category $\mathcal{C}$ consists of an endo-functor $M : \mathcal{C} \to \mathcal{C}$ with two natural transformations: the unit $\eta : 1_{\mathcal{C}} \to M$ (where $1_{\mathcal{C}}$ is the identity functor on $\mathcal{C}$) and the multiplication $\mu : M^2 \to M$ (where $M^2$ is the composite functor $M \circ M$). These are required to make the diagrams below (a.k.a., coherence conditions) commute (the symbol $\cdot$ denotes the horizontal composition of natural transformations).

<figure><img src="image_2.png" /></figure>

**Example 2.3 (Maction Monad).** The maction monad (where maction stands for monoid Action) is defined as the triple $(M_T, \eta_M, \mu_M)$ such that $M_T X := T \times X$ with $T$ a monoid, the unit $\eta_M : X \to M_T X$ with $\eta_M(x) := (0, x)$; and the multiplication $\mu_M : M_T M_T X \to M_T X$ with $\mu_M((d_1, (d_2, x))) = (d_1 + d_2, x)$. The triple satisfies the monadic laws. When it is clear from the context, we remove the subscript $T$ from the functor $M_T$.
Intuitively, the maction monad models the action of the monoid on an element in X. In the case of a time monoid T and a set of processes in X, the action is to delay programs in X of a value in T. The laws of the monad capture the facts that prefixing with a 0 time is idempotent, and prefixing in sequence is equivalent to prefixing with the sum.

Dually, comonads arise through categorical dualisation (reversing arrows in definitions), and they model contexts or environments in which computations occur. While monads abstract over producing effects (e.g., modifying state), comonads describe consuming or observing them (e.g., reading from a shared environment, or co-recursive streams). This duality enriches the categorical perspective, showing that effects are not merely one-way but can be symmetrically analysed in terms of both production and observation.

**Definition 2.4.** A comonad on a category $\mathbb{C}$ consists of an endofunctor $W : \mathbb{C} \to \mathbb{C}$ with two natural transformations: the counit $\epsilon : W \to 1_{\mathbb{C}}$ and the comultiplication $\delta : W \to W^2$. These are required to make the diagrams below commute.

<figure><img src="image_3.png" /></figure>

**Example 2.5.** The evolution comonad is the triple $(W_T, \epsilon_W, \delta_W)$ such that $W_T X := T \to (X + 1)$, the counit $\epsilon_W : W_T X \to X$ with $\epsilon_W(e) := e(0) \in X$; and the comultiplication $\delta_W : W_T X \to W_T W_T X$ with $\delta_W(e) = \lambda t, \lambda u, e(t + u)$. The triple satisfies the comonadic laws. When it is clear from the context, we remove the subscript $T$ from the functor $W_T$.

Intuitively, the evolution comonad captures the passing of time of a program. Given a state in X, and a time duration $t \in T$, the comonad returns a new state in X for which $t$ units have passed. Again, the laws are quite intuitive: a duration of 0 time does not change the state; and a sum duration can be sequenced into two durations.

The so-called Kleisli construction provides a powerful way to model computational effects in programming languages. For a monad, the Kleisli category captures effectful computations by treating morphisms as functions that return wrapped values, seamlessly chaining operations while hiding the plumbing of side effects. Dually, the Kleisli category of a comonad encodes context-dependent computations such as environments where programs read from an implicit context. When a comonad distributes over a monad, these ideas combine: the resulting Kleisli category elegantly handles programs that both produce effects (via the monad) and consume contexts (via the comonad) [20]. This is useful in concrete cases, e.g., a program might track mutable state (monadic) while accessing a read-only configuration (comonadic). By abstracting these interactions categorically, we gain a unified framework to reason about complex behaviours compositionally, ensuring cleaner semantics and more maintainable code.

**Definition 2.6.** Given a monad $(M, \eta, \mu)$ on a category $\mathbb{C}$, an M-algebra consists of an object $A \in \mathbb{C}$ (the carrier) and a morphism

$\alpha : MA \to A$ (the structure map) satisfying the following coherence conditions:

<figure><img src="image_4.png" /></figure>

In denotational semantics, M-algebras model interpretations of effectful programs: The carrier $A$ represents a semantic domain; The map $\alpha : MA \to A$ collapses effectful computations (MA) into their observable meanings (A). The coherence conditions ensure that the interpretation respects monadic structure. For example, if $M$ is the state monad, an M-algebra provides a way to evaluate stateful programs into final results by supplying an initial state.

**Example 2.7.** The maction monad leads to a $M_T$-algebra, where equations in definition 2.6 hold. Intuitively, the maction monad is acting on a state in X by adding a delay from T. The equations from the M-algebra impose that the definition of $\alpha$ must coincide with the intuitive invariants of the monadic laws.

The Eilenberg-Moore category of a monad provides a principled way to study the algebraic structure of effectful computations in programming. Where the Kleisli category focuses on how to build programs with effects, the Eilenberg-Moore category captures how to interpret or evaluate them, providing a semantic space where effectful computations can be collapsed into pure results. Each object of this category represents a domain (e.g., a type of values) equipped with a structured way to eliminate effects (e.g., running a stateful computation to produce a final output). It allows us to reason about program equivalence (when do two stateful programs produce the same result?), or even optimize effectful code (when can we safely merge or reorder operations?).

**Definition 2.8.** Given a comonad $(W, \epsilon, \delta)$ on a category $\mathbb{C}$, a W-coalgebra consists of an object $C \in \mathbb{C}$ (the carrier) and a morphism $\gamma : C \to WC$ (the structure map) satisfying the following coherence conditions:

<figure><img src="image_5.png" /></figure>

In operational semantics, W-coalgebras model stateful systems and their stepwise behavior: The carrier $C$ represents a configuration space (e.g., program states, memory layouts); The map $\gamma : C \to WC$ decomposes a state into its contextual observations (e.g., current value and remaining computation). The coherence conditions ensure consistency. For example, if $W$ is the stream comonad, a W-coalgebra describes a program as a generator of infinite outputs (e.g., a reactive system).

The co-Eilenberg-Moore category of a comonad provides a structured way to reason about programs that depend on their environment or produce results incrementally. Where the Eilenberg-Moore category allows us to interpret effectful programs by collapsing
them into final results, the co-Eilenberg-Moore category helps us de-
construct programs that rely on external inputs or generate outputs
over time. This provides a mean to design and reason about sys-
tems where behaviour depends on dynamic environments, ensuring
compositionality while maintaining clear operational meaning.

*Example 2.9.* Dually to the $M_T$-algebra, the evolution comonad leads to $W_T$-coalgebra where equations in Definition 2.8. Again, those equations force that the comonadic operations and the morphism from the $W_T$-coalgebra agree.

*Definition 2.10.* Given a distributive law $N: MW \Rightarrow WM$ of a monad $(M, \eta, \mu)$ over a comonad $(W, \varepsilon, \delta)$, an *N*-bialgebra consists of: an object $B \in \mathbb{C}$, an *M*-algebra $\alpha: MB \to B$, and a *W*-coalgebra $\gamma: B \to WB$ such that the following diagram commutes:

<figure><img src="image_6.png" /></figure>

In program semantics, *N*-bialgebras serve as mediation struc-
tures between: the denotational semantics (via the *M*-algebra $\alpha$)
expressing how to evaluate effectful computations (*MB*) to produce
final results (*B*); the operational semantics (via the *W*-coalgebra $\gamma$)
expressing how to observe stepwise behavior (*WB*) of the same pro-
gram. The distributive law *N* ensures that effect handling (*M*) and
context dependence (*W*) interoperate coherently. The commuting
diagram enforces consistency, i.e., running effects ($\alpha$) and observ-
ing steps ($\gamma$) agree when composed. This is crucial for proving
correctness of compilers (denotational models match operational
traces).

*Example 2.11.* Based on the $M_T$ maction monad and the $W_T$ evolution comonad just defined, the following is a distributive law $\xi: M_T W_T \Rightarrow D_T M_T$, such that:

$$
\xi: (d, e) \mapsto \lambda t, \begin{cases} \text{Some } (d-t, e(0)) & \text{if } d \le t \text{ and } e(d-t) \ne \text{None} \\ \text{Some } (0, e(d-t)) & \text{if } d > t \text{ and } e(d-t) \ne \text{None} \\ \text{None} & \text{if } d < t \text{ and } e(d-t) = \text{None} \end{cases}
$$

Intuitively, the distributive law mimics that time is first consumed
by the delay, and then moved forward in the evolution *e*. The
resulting *N*-bialgebra built with $\xi$ enforces consistency conditions
between the denotational semantics and the operational semantics.

3 Real-Time computation

We study a formal semantics for a language that has access to
the value in the TSC register. As expected, such semantics must
take into account that the value changes along the execution of
a program. We first present standard syntactical constructs for
integer arithmetic. Then, we give a denotational semantics for
timing delay (parametric with an architecture) as a *M*-algebra, and
an operational semantics for the state changes over the evolution
of time as a *W*-coalgebra.

The fact that the two semantics coincide is stated as a *N*-bialgebra,
with *N* a distributive law of the maction monad over the evolution
comonad.

The workflow would be as follows: a programmer writes a pro-
gram in the syntax introduced below, and the denotational seman-
tics generates a new program with additional delays given by a
model of the architecture. The newly generated program is then
analyzed with the operational semantics defined coalgebraically.

3.1 Bialgebraic semantics

*Syntax.* Terms denote arithmetic expressions, with the addition of a *now* variable that captures the passage of time:

$$
t := \mathbf{now} \mid \mathbf{var} x \mid c \mid t_1 + t_2 \mid t_1 \times t_2
$$

with $x \in \mathbb{N}$ a natural number that identifies a variable, $c$ a constant, and now the variable name for the value in the time register.
Programs are built out of standard imperative control structures:

$$
S := \mathbf{if} \ b \ \mathbf{then} \ S_1 \ \mathbf{else} \ S_2 \ \mathbf{fi} \ | \ S_1; S_2 \ | \ x := t \ | \ \mathbf{delay} \ n
$$

with *t* is a term, *x* is a variable name, and *b* a boolean condition over terms.

We introduce a loop operator on top of the language, where:

$$
\mathbf{loop} \ 0 \ p := p
$$

$$
\mathbf{loop} \ (n + 1) \ p := p; \mathbf{loop} \ n \ p
$$

A time-sensitive semantics for such language must carefully
propagate the effect of each instruction on the volatile memory
variable *now*, such that later access to that variable carries time
changes.

*Evaluation of terms.* We fix the state to be a pair of a natural value in $\mathbb{N}$ (representing the TSC counter), and a memory map from addresses to values in $\mathbb{N} \to \mathbb{N}$. We define *eval* inductively on the structure of a term, given a state $s: \mathbb{N} \times (\mathbb{N} \to \mathbb{N})$:

$$
\mathit{eval} \ c \ s ::= c
$$

$$
\mathrm{eval} \ (t_1 + t_2) \ s ::= (\mathrm{eval} \ t_1 \ s) + (\mathrm{eval} \ t_2 \ s)
$$

$$
\mathrm{eval} \ (t_1 \times t_2) \ s ::= (\mathrm{eval} \ t_1 \ s) \times (\mathrm{eval} \ t_2 \ s)
$$

$$
\mathit{eval} \ now \ s ::= \mathit{fst} \ s
$$

$$
\mathit{eval} \ (\mathit{var} \ n) \ s ::= \mathit{snd} \ s \ n
$$

*Operational semantics.* We give an operational semantics for the syntax introduced just before. We use the evolution comonad $E_N$ as introduced in Example 2.9, and fix the carrier to be the pair of a program and a state. Figure 2 introduces an intermediate function $[\cdot:]$ that evaluates a program statement, with a state $s$, and a time duration $t$. All steps are standard, except for the delay statement and the sequential composition. The delay statement will be rewritten to take into account the time that passes. The sequential statement first evaluates the left part, and then the right part with the remaining time. Note that the output of the $[\cdot:]$ is a triple: the last element of the triple is the remaining time value after executing the program $p$ in state $s$ with initial amount of time $t$.

The two function *update_time* and *update_var* are left abstract for now. The former updates the state given the time that passes, and the latter updates the state variables when an assignment occurs. Finally, the *eval* function is the standard boolean evaluation function for guards.
$$ [[\mathbf{if} \ b \ \mathbf{then} \ S_1 \ \mathbf{else} \ S_2 \ \mathbf{fi}, s, t]] ::= \mathbf{if} \ (\mathbf{eval} \ b \ s) \ \mathbf{then} \ [[S_1, s, t]] \ \mathbf{else} \ [[S_2, s, t]] $$

$$ [[S_1; S_2, s, t]] ::= \begin{cases} [[S'_1; S_2, s', 0]] & \mathbf{if} \ [[S_1, s, t]] = (S'_1, s', 0) \\ [[S_2, s', t')] & \mathbf{if} \ [[S_1, s, t]] = (S'_1, s', t') \text{ with } t' \neq 0 \end{cases} $$

$$ [[\mathbf{delay} \ n, s, t]] ::= \begin{cases} (\mathbf{delay} \ (n-t), \mathbf{update\_time} \ s \ t, 0) & \mathbf{if} \ t \leq n \\ (\mathbf{delay} \ 0, \mathbf{update\_time} \ s \ n, t-n) & \mathbf{else} \ 0 \end{cases} $$

$$ [[x := e, s, t]] ::= (\mathbf{delay} \ 0, \mathbf{update\_var} \ x \ e \ s, t). $$

<caption>Figure 2: Semantic rules</caption>

We instantiate the operational semantics as a $E_N$-coalgebra with

* carrier as elements in the product type $P \times state$, and

* morphism $\alpha : P \times state \to E_N(P \times state)$ with

$$ \alpha(p, s) = \lambda t, \text{ Some } (\mathbf{fst} \ [[p, s, t]]) $$

We can prove that $(P \times state, \alpha)$ is a $E_N$-coalgebra, which requires first that $\alpha$ satisfies the right identity axiom, i.e.

$$ \alpha(p, s) = 0 \quad (p, s) $$

and that

$$ \alpha(p, s) (t + t') = \alpha(\alpha(p, s) t) t' $$

The first axiom, intuitively, forces a self loop transition when no time passes. The second axiom enforces that, given a composite time $t + t'$, the final state is the same whether we run the process in “temporal” sequence (i.e., first with $t$ units, and then with $t'$ units) or once in a row (i.e., $t + t'$ units).

Several intermediate lemma were necessary to prove the two laws of the coalgebra. For instance:

$$ [[p, s, t]] = (p', s', c) \wedge c \neq 0 \implies \forall n, [[p', s', n]] = (p', s', n). $$

Intuitively, it means: if the execution of a program $p$ in state $s$ terminates with a time strictly lower than $t$, then running the terminated program will not make any progress.

**Denotational semantics.** We now introduce an algebra over the programming language, that values the timing delay of a program in terms of the delay introduced by each primitives in the targeted architecture. We first introduce a delay function $\beta$, defined with:

$$ \beta t p = \begin{cases} p & \mathbf{if} \ t = 0 \\ \mathbf{delay} \ t; \mathbf{if} \ b \ \mathbf{then} \ S_1 \ \mathbf{else} \ S_2 & \mathbf{if} \ p = \mathbf{if} \ b \ \mathbf{then} \ S_1 \ \mathbf{else} \ S_2 \\ \mathbf{delay} \ t; \ n := e & \mathbf{if} \ n := e \\ (\beta t S_1); \ S_2 & \mathbf{if} \ p = S_1; \ S_2 \\ \mathbf{delay} \ (n+t) & \mathbf{if} \ p = \mathbf{delay} \ n \end{cases} $$

Intuitively, $\beta$ prefixes a program with a delay taken as parameter. The delay could model the time that a previous instruction has taken to execute.

The definition of the $M$-algebra with carrier the set of program terms, and with morphism $\beta : MP \to P$ is such that the following two axioms must hold:

$$ \beta 0 p = p $$

and

$$ \beta (n_1 + n_2) p = \beta n_1 (\beta n_2 p) $$

Both are intuitive, in the sense that prefixing a 0 delay should return the same program, and prefixing a sum of two delays should be the same as doing the prefixing in sequence.

We lift the $M$-coalgebra to one that acts on a pair of a program $P$ and a state in state.

**Relating the operation and the denotation.** We combine the two semantics into a bialgebra, given by the distributive law of the maction monad over the evolution comonad. Such bialgebra comes with one proof obligation, which requires two lemmas on the relation between the $E_N$-coalgebra $(P \times state, \alpha)$ and the $M$-algebra $(P \times state, \beta)$.

The proof obligation relates $\alpha$ and $\beta$ such that:

$$ \alpha(\beta n p) s t = \begin{cases} (\beta (n-t) p, s) & \mathbf{if} \ t \leq n \\ \alpha p s (t-n) & \mathbf{if} \ n < t \end{cases} $$

Intuitively, this means that if we add a delay $n$ to a program $p$ from state $s$ and run the resulting program during $t$ unit of time, then:

* if $t \leq n$, then this gives the same as adding the delay resulting from $n-t$;

* otherwise, the result is that same as running the program $p$ in state $s$ during $t-n$ unit of times.

To prove the case for $t \leq n$, we need:

$$ \pi_1(\alpha (\beta n p) s t) = (\beta (n-t) p, s) $$

To prove the case for $n < t$, we need:

$$ \pi_1(\alpha p s (t-n)) = \pi_1(\alpha (\beta n p) s t) $$

In order to prove the relation between $\alpha$ and $\beta$, two axioms have to be established:

$$ \forall p, (\mathbf{delay} \ 0; p) = p \qquad (1) $$

$$ \forall s t, \mathbf{update\_time} \ s t = s \qquad (2) $$

Axiom (2) imposes a strong condition namely that the time that passes should not change the value of the state. This should have been expected, as the monad operation is completely oblivious to the state. We discuss in Section 4 necessary assumptions to relax this requirement.

## 3.2 Formalization in Rocq

The Rocq proof assistant is a rich environment to formalize the present theory. Built on top of the calculus of inductive construction and dependent type theory, each categorical construct has an intuitive representation as a dependent term.
For instance, the general definition of a monad is represented in Rocq as a record type:

Record MONAD (C : CATEGORY) : Type := {
  monad :> FUNCTION C C;
  ret : NT (f_id C) monad;
  mult : NT (f_comp monad monad) monad;
  mult ret : forall X,
    comp (mult X) (f_mor (ret X)) = id;
  ret_mult : forall X,
    comp (mult X) (ret (monad X)) = id;
  mult_mult : forall X,
    comp (mult X) (f_mor (mult X)) =
    comp (mult X) (mult (monad X))
}.

where the first three fields correspond to the monad functor, the
return and multiplication natural transformations; and the last three
fields are the axioms that the monad must satisfy, as detailed in
definition 2.2.

The maction monad (defined in Rocq as maction_monad) is an instance of the monad definition, given by the following:

Program Definition maction_monad {T:timedomain} : MONAD
    Ens := {
        monad := maction_funct T;
        ret := maction_unit T;
        mult := maction_mult T
    }.

where the three obligations must be proven after closing the defini-
tion.

The language is defined as an inductive datatype:

Inductive prog : Type :=
| ife : prim -> prog -> prog -> prog
| assign : nat -> prim -> prog
| pseq : prog -> prog -> prog
| delay : nat -> prog.

where prim are primitive expressions.

The denotational semantics is given with the maction monad
algebra as

Program Definition add_state : Malgebra maction_monad :=
    {
        car := (prog * state)%type;
        tmor := fun s =>
            (add_delay_prefix (fst s) (fst (snd s))), (snd (snd s)))
    }.

All obligations from the definition of the Malgebra must be proved
in Rocq for the definition to be accepted by Rocq.

The operational semantics is given with the evolution coalgebra
as

Program Definition WCoalg_Prog : WCoalgebra (@tev_comonad
DTime) :=
{
  Wcoalg :=
  {
    ccar := (prog * state)%type;
    kmor := fun p =>
      (| tevolutionFun := fun t => Some (fst (
        evolve (fst p) (snd p) t));
        zero_val := fst (evolve (fst p) (snd p) 0)
      |}
  }
}.

The codomain of the coalgebra morphism has several additional obli-
gations, that are specific to the definition of the evolution comonad.
Once again, obligations must be proved in Rocq for the definition
to be accepted.

Finally, the bialgebra semantics is defined as an instance of the
bialgebra with the distributive law of the maction monad over the
evolution comonad:

Program Definition lbialg Semantics : lbialgebra
    distr_MAct_Evolution := {
        car_bialg := (prog * state)%type;
        h_bialg := add_state;
        k_bialg := WCoalg_Prog;
    }.

The richness of a proof assistant based on dependent type helps
to formalize precisely each mathematical construct, and keeps track
of all necessary proof requirements. Based on the formalized the-
ory, we show the necessary extensions for the construction and
certification of a time-aware compiler.

4 Towards certification of a time-aware compiler

In this section, we give a road-map to extend the framework pre-
sented in Section 3 in order to certify a compiler for real-time
applications. We first define compilation categorically, as a coalge-
bra morphisms with a bisimulation relation between the input and
output morphisms. We then present specific challenges in having
a certified compiler, as time is volatile and dependent on the tar-
geted architecture. Finally, we discuss the steps towards a certified
compiler for real-time systems, using the categorical framework
introduced in Section 3.

4.1 Compilation Categorically

A W-coalgebra morphism between coalgebra (X, α₁) and (Y, α₂) is
a morphism Y : X → Y such that the following diagram commutes

<figure><img src="image_7.png" /></figure>

A compiler can therefore be defined as a coalgebra morphism,
i.e., a transformation $\gamma$ where

• $\gamma: X \to Y$ compiles an object from the input domain in $X$
  to an output object in $Y$;

• $\alpha_1$ and $\alpha_2$ are respectively the operational semantics of the
source and target objects;

The commuting of the diagram ensures that the operational
semantics of the input and target languages coincide. A trivial
example of a compiler would be the one that uniformly maps all
programs in X to a void program in Y. The diagram would trivially
commute, but such compiler would be entirely useless. We need
an additional concept of bisimulation to fully characterize what a
compiler must do, i.e., preserve the semantics.

A bisimulation is a coalgebra (R, o) such that the following dia-
gram commutes:
<figure><img src="image_8.png" /></figure>

where $\pi_1$ and $\pi_2$ are projections from the carrier $R$ to $X$ and $Y$ respectively. The existence of such bisimulation precludes the trivial map $\gamma$ as the two observables from the coalgebra $\alpha_S$ and $\alpha_T$ must now be in relation.

The definition of a compiler $\gamma$, together with the existence of a bisimulation between the source and target coalgebras is therefore the prime challenge for compiler correctness for timed-sensitive programs.

## 4.2 Real-time considerations

In order to achieve the main goal of certification of a time-aware compiler, we discuss challenges related to the target operational semantics, and necessary amendments to the model introduced in Section 3.

**Target dependency.** In modern architectures (such as x86 processors), there is direct access to a register, called Time Stamp Counter (TSC) that counts clock cycles from booting time. The instruction `__rdtsc()` fetches and returns the current value of the TSC register.

The TSC register is of size 64 bits and the program in Listing 2 aims at storing, in the rec array, the delay between two consecutive readings of the TSC register. The loop records a series of measures on the register `__rdtsc()`, which are representative of the architecture and runtime environment on which the program will be executed. Such practical experiments highlight real-time features emerging from running programs on modern architectures.

The compiled version of the code in Listing 2 is given without optimization with modern gcc compiler for Intel x86 architecture. The code in Listing 3 shows the assembly code for the measuring loop of Listing 2.

```c
volatile uint64_t rectime1, rectime2;
uint64_t *rec = malloc(end*sizeof(uint64_t));
for (int i=0; i < end; i++) {
    rectime1 = __rdtsc();
    rectime2 = __rdtsc();
    rec[i] = rectime2 - rectime1;
}
```

### Listing 2: C program for reading the TSC register

As expected, two readings of the time stamp counter (rdtsc) are separated with some operations on the rdx and rax registers.

The salq operation shifts the least 32 bits from the rdx registers to the most significant 32 bits

Then, the orq operation performs an OR between the rdx and rax register, such that rax now stores the whole value from the time stamp counter.

The value from the rax register is moved onto the stack with the movq operation.

The same operations are repeated after the second rdtsc instruction. Then, the loop counter is updated and the conditional jump brings back to the beginning of the loop.

L2:

<figure><img src="image_9.png" /><figcaption>Figure 3: Histogram for consecutive time readings</figcaption></figure>

```
rdtsc      $32, %rdx
salq       $32, %rdx
orq        %rdx, %rax
movq       %rax, (%rsp)
rdtsc
salq       $32, %rdx
addq       $8, %rcx
orq        %rdx, %rax
movq       %rax, 8(%rsp)
movq       8(%rsp), %rax
movq       (%rsp), %rdx
subq       %rdx, %rax
movq       %rax, -8(%rcx)
cmpq       %rbp, %rcx
jne         .L2
```

### Listing 3: Compiled with gcc

Running the code above on a Linux operating system gives the histogram (cropped at 100 on the y-axis) in Figure 3. As a first observation, the mean and average value are close to each others, around 15 clock cycles. However, some artefacts are clearly visible, which are not reflected neither in the C code, nor in the assembly code.

We describe hereafter the main changes we foresee to the semantic model in order to include time-dependent memory operations in the language (e.g., read of the TSC register).

More precisely, axiom (2) states that the passing of time cannot change the value of the state. This axiom follows from the requirements that the distributive law impose on the update function. In the objective to relate the input language semantics to the target object semantics, the passing of time at the architecture level is given by a register (namely, the time stamp counter). We foresee a need to change the monad, comonad, and distributive law introduced in the current framework, to permit time dependent modification of the register value. This would extend the current expressiveness of the language, with access to a memory variable (e.g., TSC register) whose value would change depending on time.

Concretely, the current distributive law imposes the following invariant:

$$ \alpha (\beta n p) s (n + 1) = \alpha p s 1 $$
One should extend the definitions of $\alpha$, $\beta$, and the distributive law in order to allow the state to change over time. Hence, in this modified framework, delaying from *n* units of time and waiting for *n* units would change the state *s* and would be different from executing *p* without delay for 1 units.

# 5 Related work

**Formal compiler and correctness.** The field of formal verification mainly considers the logical effects of programs. Compilers such as CompCert or CakeML are a formalization of a C compiler and ML compiler respectively. The semantic preservation theorem of CompCert and CakeML shows that a functional description can be compiled to an imperative program while preserving the input/output behaviour. The two compilers do not yet deliver certificates about time guarantees. As CompCert explicitly says in its documentation, the semantic preservation theorem ensures that observable behaviours of the source and target programs are the same, and define observable behaviour as “everything the user of the program, or the physical world in which it executes, can ‘see’ about the actions of the program, with the notable exception of execution time and memory consumption” [22]. The approach discussed here makes time an observable behaviour. Several works have studied extensions of the CompCert semantic preservation theorem for constant time complexity preservation [4] and worst case analysis [14]. The formalisation of time as an effect, and the use of categorical framework can be the “formal framework” that will be used as a standard for other formalisation for compositional verification. Frameworks used by industrial such as Frama-C or KataOS (Google) would also benefit from such a framework.

**Space and timing guarantees.** Most proof systems focus on space guarantees, i.e., safe allocation of memory at runtime. Languages such as Rust are popular since they enforce at the design level some properties about memories. The type theory underlying the type system of Rust is a recent work that focuses on memory ownership and management. Logics such as separation logic [17] is one instance of a logic that provides primitives to prove memory isolation and heap invariant.

To reason about time at the type system level is a new challenge that would also benefit the ecosystem of programming languages. Until now, time is essentially abstracted as a logical step in synchronous languages such as LUSTRE [24]. However, the presence of physical components interacting with a program renders logical time inadequate for analysis. Instead, safety for cyber-physical systems requires precise physical time [12]. The formal semantics developed in this project will provide an intermediate representation for more abstract descriptions such as in Platzer with its formal framework for analysis of cyber-physical systems [18], Naijun Zhang with the formalization of hybrid systems [27], and Edward Lee with an actor-based implementation of hybrid systems [13]. The quantum physicist Nicolas Gisin also witnesses that using computational model for explaining physics is a region rich of theoretical and practical questions, fertile for discoveries [5].

**Categorical modeling of Timed-Processes.** The notion of a bialgebra was coined in [19] to describe “well-behaving” operational semantics. In their paper, the monad corresponds to the syntactic

functor to construct program terms, and the comonad captures the structural operational semantics. The bialgebra established “well-behaving” conditions between the denotational and operational semantics. The work has been applied in [9] to model timed processes categorically. More precisely, the focus is made on algebra of processes, such as extension of CCS with time. In the present work, we consider imperative and stateful languages. Extension to relate EilenbergMoore category and Kleisli category have been developed, for instance in [8]. Since the Kleisli category has a natural interpretation as a computational domain (morphisms are effectful computations), it is of relevance to find how such categories relate to the present work, such as in [6].

**Static Analysis.** Analysis on the worst case execution time have been performed on annotated programs, and CompCert has been used to preserve the real-time guarantees of such annotated programs. Research in the field has lead to the AbsInt company [21], that develops techniques based on abstract interpretation to analyse the worst case execution time (WCET) of dedicated software [26]. Current research explore parametric WCET [7], where the worst-case execution time of a program is expressed as a function of its arguments. Our approach aims to give a compositional and time-sensitive semantics. Compilation and preservation of real time guarantees such as those imposed by the language timedC [16] stands as a direct future application of our work.

# 6 Conclusion

The development of a certified compiler for time-aware computation demands rigorous mathematical foundations to ensure precise and verifiable timing guarantees. In this work, we have demonstrated that category theory, particularly through the use of monads, comonads, and bialgebras, provides a powerful semantic framework for modeling and reasoning about real-time program behavior.

While we have established the core theoretical framework, several challenges remain. Future work includes refining the interaction between time-dependent state updates and the distributive laws governing program semantics, as well as extending the model to support more complex timing constraints and architectural dependencies. Additionally, integrating our formalism with existing certified compiler infrastructures (e.g., CompCert) could pave the way for practical applications in real-time embedded systems and cyber-physical systems.

Ultimately, this work lays the groundwork for a new generation of verified compilers that not only preserve functional correctness but also enforce timing guarantees. It is a critical step toward safer and more predictable real-time software. By continuing to explore the rich interplay between category theory and program semantics, we aim to bridge the gap between abstract mathematical models and the concrete demands of time-sensitive computing.

**Acknowledgement.** Benjamin Lion was part of the Cert-T project, funded by the European MSCA-PF grant agreement 101153247.

# References

[1] Reynald Affeldt, Jacques Garrigue, David Nowak, and Takafumi Saikawa. 2021. A trustful monad for axiomatic reasoning with probability and nondeterminism. *J. Funct. Program.* 31 (2021), e17. doi:10.1017/S0956796821000137

[2] Reynald Affeldt and David Nowak. 2020. Extending Equational Monadic Reasoning with Monad Transformers. In *26th International Conference on Types for*
*Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy (LIPICS, Vol. 188), Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2:1-2:21. doi:10.4230/LIPICS TYPES. 2020.2*

[3] Reynald Affeldt, David Nowak, and Takafumi Saikawa. 2019. A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning. In *Mathematics of Program Construction - 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019, Proceedings (Lecture Notes in Computer Science, Vol. 11825)*, Graham Hutton (Ed.). Springer, 226-254. doi:10.1007/978-3-030-33636-3_9

[4] Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu. 2020. Formal verification of a constant-time preserving C compiler. *Proc. ACM Program. Lang.* 4, POPL (2020), 7:1-7:30. doi:10.1145/3371075

[5] Nicolas Gisin. 2021. Indeterminism in Physics, Classical Chaos and Bohmian Mechanics. Are Real Numbers Really Real? *Erkenntnis* 86 (12 2021). doi:10.1007/s10670-019-00165-8

[6] Sergey Goncharov, Renato Neves, and José Proença. 2020. Implementing Hybrid Semantics: From Functional to Imperative. In *Theoretical Aspects of Computing - ICTAC 2020 - 17th International Colloquium, Macau, China, November 30 - December 4, 2020, Proceedings (Lecture Notes in Computer Science, Vol. 12545)*, Violet Ka I Pun, Volker Stolz, and Adenilso Simão (Eds.). Springer, 262-282. doi:10.1007/978-3-030-64276-1_14

[7] Sandro Grebant, Clément Ballabriga, Julien Forget, and Giuseppe Lipari. 2024. Parametric WCET as a function of procedure arguments: Analysis and applications. *Journal of Systems Architecture* 148 (2024), 103086. doi:10.1016/j.sysarc.2024.103086

[8] Bart Jacobs. 2015. Dijkstra and Hoare monads in monadic computation. *Theor. Comput. Sci.* 604 (2015), 30-45. doi:10.1016/J.TCS.2015.03.020

[9] Marco Kick, John Power, and Alex Simpson. 2006. Coalgebraic semantics for timed processes. *Inf. Comput.* 204, 4 (2006), 588-609. doi:10.1016/J.IC.2005.11.003

[10] Xavier Leroy. 2009. A formally verified compiler back-end. *Journal of Automated Reasoning* 43, 4 (2009), 363-446. http://xavierleroy.org/publi/compcert-backend.pdf

[11] Benjamin Lion. 2025. Rocq artifact for Bialgebraic semantics. doi:10.5281/zenodo.16872463

[12] Benjamin Lion, Farhad Arbab, and Carolyn L. Talcott. 2022. A semantic model for interacting cyber-physical systems. *J. Log. Algebraic Methods Program.* 129 (2022), 100807. doi:10.1016/J.JLAMP.2022.100807

[13] Marten Lohstroh, Christian Menard, Soroush Bateni, and Edward A. Lee. 2021. Toward a Lingua Franca for Deterministic Concurrent Systems. *ACM Trans. Embed. Comput. Syst.* 20, 4 (2021), 36:1-36:27. doi:10.1145/3448128

[14] André Oliveira Maroneze. 2014. Certified Compilation and Worst-Case Execution Time Estimation. (Compilation formellement vérifiée et estimation du pire temps d'exécution). Ph. D. Dissertation. University of Rennes 1, France. https://tel.archives-ouvertes.fr/tel-01064869

[15] Eugenio Moggi. 1991. Notions of Computation and Monads. *Inf. Comput.* 93, 1 (1991), 55-92. doi:10.1016/0890-5401(91)90052-4

[16] Saranya Natarajan and David Broman. 2018. Timed C: An Extension to the C Programming Language for Real-Time Systems. In *IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2018, 11-13 April 2018, Porto, Portugal*, Rodolfo Pellizzoni (Ed.). IEEE Computer Society, 227-239. doi:10.1109/RTAS.2018.00031

[17] Peter W. O'Hearn. 2007. Resources, concurrency, and local reasoning. *Theor. Comput. Sci.* 375, 1-3 (2007), 271-307. doi:10.1016/J.TCS.2006.12.035

[18] André Platzer. 2018. Logical Foundations of Cyber-Physical Systems. Springer. doi:10.1007/978-3-319-63588-0

[19] Daniele Turi and Gordon D. Plotkin. 1997. Towards a Mathematical Operational Semantics. In *Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997*. IEEE Computer Society, 280-291. doi:10.1109/LICS.1997.614955

[20] Tarmo Uustalu and Varmo Vene. 2005. The Essence of Dataflow Programming. In *Programming Languages and Systems, Third Asian Symposium, APLAS 2005*, Tsukuba, Japan, November 2-5, 2005, *Proceedings (Lecture Notes in Computer Science, Vol. 3780)*, Kwangkeun Yi (Ed.). Springer, 2-18. doi:10.1007/11575467_2

[21] Absint website. 2025. Static Time analysis in Absint. https://web.archive.org/web/20250624172030/https://www.absint.com/ait/

[22] Compcert website. 2025. Context and motivations. https://web.archive.org/web/20250126133341/https://compcert.org/motivations.html

[23] Sel4 website. 2021. More Research. https://web.archive.org/web/20240114071833/https://sel4.systems/About/more-research.pml

[24] Verimag website. 2025. The Lustre Programming Language. https://web.archive.org/web/20250419120230/https://www-verimag.imag.fr/The-Lustre-Programming-Language-and

[25] Reinhard Wilhelm. 2020. Real time spent on real time. *Commun. ACM* 63, 10 (Sept. 2020), 54-60. doi:10.1145/3375545

[26] Reinhard Wilhelm, Jakob Engblom, Andreas Ermedahl, Niklas Holsti, Stephan Thesing, David B. Whalley, Guillem Bernat, Christian Ferdinand, Reinhold Heckmann, Tulika Mitra, Frank Mueller, Isabelle Puaut, Peter P. Puschner, Jan Staschulat, and Per Stenström. 2008. The worst-case execution-time problem - overview of methods and survey of tools. *ACM Trans. Embed. Comput. Syst.* 7, 3 (2008), 36:1-36:53. doi:10.1145/1347375.1347389

[27] Xiong Xu, Jean-Pierre Talpin, Shuling Wang, Bohua Zhan, and Naijun Zhan. 2023. Semantics Foundation for Cyber-physical Systems Using Higher-order UTP. *ACM Trans. Softw. Eng. Methodol.* 32, 1 (2023), 9:1-9:48. doi:10.1145/3517192