Clocked lambda calculus

DOI10.1017/S0960129515000389MaRDI QIDQ5269007zbMATH OpenOpenAlexFDO

Authors Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, Andrew Polonsky

Publication date 14 June 2017

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1405.7500

zbMATH Keywords

lambda calculusBöhm treesclocked lambda calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

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

• Discriminating lambda-terms using clocked Böhm trees
• Highlights in infinitary rewriting and lambda calculus
• Infinitary lambda calculus and discrimination of Berarducci trees.
• The infinitary lambda calculus of the infinite eta Böhm trees
• scientific article; zbMATH DE number 2090071

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)

• scientific article; zbMATH DE number 445159 (Why is no real title available?)
• Clocks for Functional Programs
• Infinitary lambda calculus and discrimination of Berarducci trees.
• Discriminating lambda-terms using clocked Böhm trees

Describes a project that uses

Uses Software

• Automath

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)