An Introduction to the Clocked Lambda Calculus
Logic in Computer Science
2015-10-21 v1
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.
Cite
@article{arxiv.1405.7500,
title = {An Introduction to the Clocked Lambda Calculus},
author = {Jörg Endrullis and Dimitri Hendriks and Jan Willem Klop and Andrew Polonsky},
journal= {arXiv preprint arXiv:1405.7500},
year = {2015}
}