  We give a brief introduction to the clocked lambda calculus, an extension of
the classical lambda calculus with a unary symbol tau used to witness the
beta-steps. In contrast to the classical lambda calculus, this extension is
infinitary strongly normalising and infinitary confluent. The infinitary normal
forms are enriched Boehm Trees, which we call clocked Boehm Trees.

Logic in Computer Science