scientific article; zbMATH DE number 7204433

DOI10.4230/LIPICS.FSCD.2017.14zbMATH Open1434.03049arXiv1306.2069MaRDI QIDQ5111310FDOQ5111310

Łukasz Czajka

Publication date: 26 May 2020

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

Title of this publication is not available (Why is that?)

Recommendations

• On the confluence of lambda-calculus with conditional rewriting
• Foundations of Software Science and Computation Structures
• Conditional linearization
• scientific article
• Confluence of the disjoint union of conditional term rewriting systems

zbMATH Keywords

combinatory logicconfluenceconditional linearizationunique normal form property

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (6)

• Extensionalism and induction in Boole
• Boolean algebra admits no convergent term rewriting system
• Title not available (Why is that?)
• Boolean negation and non-conservativity II: The variable-sharing property
• A formalisation of consistent consequence for Boolean equation systems
• Expanding \(\text{FL}_{ew}\) with a Boolean connective

Uses Software

• Coq
• CoqHammer

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5111310)