Higher-order rewrite systems and their confluence

DOI10.1016/S0304-3975(97)00143-6zbMATH Open0895.68078OpenAlexW1975808446MaRDI QIDQ1127334FDOQ1127334

Authors: Richard M. Mayr, Tobias Nipkow 

Publication date: 13 August 1998

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(97)00143-6

Recommendations

• scientific article; zbMATH DE number 1552533
• scientific article; zbMATH DE number 512788
• scientific article; zbMATH DE number 1615229

zbMATH Keywords

higher-order rewrite systems

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Cites Work

• Title not available (Why is that?)
• Isabelle. A generic theorem prover
• Title not available (Why is that?)
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Combinatory reduction systems: Introduction and survey
• 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?)
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• The Clausal Theory of Types
• Computing in systems described by equations
• The undecidability of the second-order unification problem
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Combinators, \(\lambda\)-terms and proof theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• The variable containment problem
• Linear unification of higher-order patterns
• Adding algebraic rewriting to the untyped lambda calculus (extended abstract)
• Confluence of the lambda calculus with left-linear algebraic rewriting
• Title not available (Why is that?)
• Title not available (Why is that?)
• A termination ordering for higher order rewrite systems
• Title not available (Why is that?)
• Confluence and superdevelopments
• Towards a domain theory for termination proofs

Cited In (59)

• Formally verified animation for RoboChart using interaction trees
• Sharing proofs with predicative theories through universe-polymorphic elaboration
• Perpetuality and uniform normalization in orthogonal rewrite systems
• Title not available (Why is that?)
• Confluence by critical pair analysis revisited
• Superposition with lambdas
• Inductive-data-type systems
• Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding
• Unifying sets and programs via dependent types
• 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?)
• Pushing the frontiers of combining rewrite systems farther outwards
• Algebraic coherent confluence and higher globular Kleene algebras
• Infinitary combinatory reduction systems
• The variable containment problem
• Processes, Terms and Cycles: Steps on the Road to Infinity
• PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
• Rewriting, and equational unification: the higher-order cases
• Title not available (Why is that?)
• Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules
• Contextual Natural Deduction
• Title not available (Why is that?)
• Decreasing diagrams and relative termination
• Size-based termination of higher-order rewriting
• Expression reduction systems with patterns
• Nominal Confluence Tool
• Superposition with lambdas
• On the termination of Russell's description elimination algorithm
• Capture-avoiding substitution as a nominal algebra
• Superposition for higher-order logic
• Normal Higher-Order Termination
• Checking overlaps of nominal rewriting rules
• Higher-order substitutions
• Cut Elimination, Substitution and Normalisation
• Soundness and completeness proofs by coinductive methods
• Theory and practice of second-order rewriting: foundation, evolution, and SOL
• A Proof of Finite Family Developments for Higher-Order Rewriting Using a Prefix Property
• Title not available (Why is that?)
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
• How to prove decidability of equational theories with second-order computation analyser SOL
• Nominal rewriting
• A new connective in natural deduction, and its application to quantum computing
• Confluence Competition 2015
• Title not available (Why is that?)
• Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs
• Shallow confluence of conditional term rewriting systems
• n-level rewriting systems
• Higher-order superposition for dependent types
• Higher-order narrowing with convergent systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• On proving confluence modulo equivalence for Constraint Handling Rules
• Antimirov and Mosses’s Rewrite System Revisited
• A restricted form of higher-order rewriting applied to an HDL semantics
• Development closed critical pairs
• Pure pattern calculus à la de Bruijn

Uses Software

• Isabelle
• ML
• HOL
• Automath

This page was built for publication: Higher-order rewrite systems and their confluence

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