scientific article; zbMATH DE number 7204433

DOI10.4230/LIPIcs.FSCD.2017.14zbMath1434.03049arXiv1306.2069MaRDI QIDQ5111310

Łukasz Czajka

Publication date: 26 May 2020

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

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

confluencecombinatory logicconditional linearizationunique normal form property

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Uses Software

• Coq
• CoqHammer

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Conditional linearization
• Unique normal forms for lambda calculus with surjective pairing
• Hammer for Coq: automation for dependent type theory
• Term Rewriting and All That
• Open problems in rewriting
• Unique normal forms for nonlinear term rewriting systems: Root overlaps
• Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative
• Unique normal form property of compatible term rewriting systems: A new proof of Chew's theorem

This page was built for publication: