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.
Recommendations
Cites work
- scientific article; zbMATH DE number 3837349 (Why is no real title available?)
- scientific article; zbMATH DE number 6115908 (Why is no real title available?)
- scientific article; zbMATH DE number 3759516 (Why is no real title available?)
- scientific article; zbMATH DE number 1948154 (Why is no real title available?)
- scientific article; zbMATH DE number 1889386 (Why is no real title available?)
- scientific article; zbMATH DE number 937379 (Why is no real title available?)
- A-translation and looping combinators in pure type systems
- Algebraic semantics and complexity of term rewriting systems
- An extensional treatment of dataflow deadlock
- Applications of infinitary lambda calculus
- Descendants and origins in term rewriting.
- Discriminating lambda-terms using clocked Böhm trees
- Full abstraction in the lazy lambda calculus
- Infinitary combinatory reduction systems: confluence
- Infinitary lambda calculus
- LCF considered as a programming language
- Non-existent Statman's double fixed point combinator does not exist, indeed
- The absence and the presence of fixed point combinators
- The lambda calculus. Its syntax and semantics. Rev. ed.
Cited in
(4)
This page was built for publication: Clocked lambda calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5269007)
