We introduce the *clocked lambda calculus*,
an extension of the classical lambda calculus with a unary symbol \( \tau \) that serves as a witness of \( \beta \)-steps.
This calculus consists of the following two rules:
\[
\begin{aligned}
(\lambda x.M) N &\to \tau( M[x = N] ) \\
\tau(M)N &\to \tau(MN)
\end{aligned}
\]
The clocked lambda-calculus is infinitary strongly normalizing, infinitary confluent,
and the unique infinitary normal forms constitute enriched Böhm trees (more precisely, Lévy-Longo trees),
which we call *clocked Böhm trees*.
We show that clocked Böhm trees are suitable for discriminating a rich class of lambda terms having the same Böhm trees.

See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.

} }