Clocked lambda calculus

DOI10.1017/S0960129515000389zbMATH Open1387.03013OpenAlexW3104111471MaRDI QIDQ5269007FDOQ5269007

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)

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

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

zbMATH Keywords

lambda calculusBöhm treesclocked lambda calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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)

• Title not available (Why is that?)
• Clocks for Functional Programs
• Infinitary lambda calculus and discrimination of Berarducci trees.
• Discriminating lambda-terms using clocked Böhm trees

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)