Clocked lambda calculus
From MaRDI portal
Publication:5269007
DOI10.1017/S0960129515000389zbMATH Open1387.03013arXiv1405.7500OpenAlexW3104111471MaRDI QIDQ5269007FDOQ5269007
Jörg Endrullis, Jan Willem Klop, Andrew Polonsky, Dimitri Hendriks
Publication date: 14 June 2017
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1405.7500
Cites Work
- LCF considered as a programming language
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Infinitary lambda calculus
- Full abstraction in the lazy lambda calculus
- Descendants and origins in term rewriting.
- An extensional treatment of dataflow deadlock
- Infinitary Combinatory Reduction Systems: Confluence
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The absence and the presence of fixed point combinators
- Applications of infinitary lambda calculus
- Non-existent Statman's double fixed point combinator does not exist, indeed
- Algebraic semantics and complexity of term rewriting systems
- A-translation and looping combinators in pure type systems
- Discriminating Lambda-Terms Using Clocked Boehm Trees
Cited In (3)
Uses Software
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)
