An Introduction to the Clocked Lambda Calculus

Abstract

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.

References in corpus (3)

• Infinitary Combinatory Reduction Systems: Confluence
• Discriminating Lambda-Terms Using Clocked Boehm Trees
• An Introduction to the Clocked Lambda Calculus

Cited by in corpus (2)

• An Introduction to the Clocked Lambda Calculus
• Interaction Equivalence