Higher-order rewrite systems and their confluence
From MaRDI portal
Publication:1127334
Cites work
- scientific article; zbMATH DE number 2185671 (Why is no real title available?)
- scientific article; zbMATH DE number 2185672 (Why is no real title available?)
- scientific article; zbMATH DE number 3976991 (Why is no real title available?)
- scientific article; zbMATH DE number 3730111 (Why is no real title available?)
- scientific article; zbMATH DE number 108365 (Why is no real title available?)
- scientific article; zbMATH DE number 108434 (Why is no real title available?)
- scientific article; zbMATH DE number 512788 (Why is no real title available?)
- scientific article; zbMATH DE number 512795 (Why is no real title available?)
- scientific article; zbMATH DE number 599028 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 1499112 (Why is no real title available?)
- scientific article; zbMATH DE number 3993540 (Why is no real title available?)
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- A termination ordering for higher order rewrite systems
- Adding algebraic rewriting to the untyped lambda calculus (extended abstract)
- Combinators, \(\lambda\)-terms and proof theory
- Combinatory reduction systems: Introduction and survey
- Computing in systems described by equations
- Confluence and superdevelopments
- Confluence of the lambda calculus with left-linear algebraic rewriting
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Isabelle. A generic theorem prover
- Linear unification of higher-order patterns
- The Clausal Theory of Types
- The lambda calculus. Its syntax and semantics. Rev. ed.
- The undecidability of the second-order unification problem
- The variable containment problem
- Towards a domain theory for termination proofs
Cited in
(60)- Formally verified animation for RoboChart using interaction trees
- Sharing proofs with predicative theories through universe-polymorphic elaboration
- Finite family developments
- Higher-order superposition for dependent types
- scientific article; zbMATH DE number 176122 (Why is no real title available?)
- Inductive-data-type systems
- How to prove decidability of equational theories with second-order computation analyser SOL
- Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs
- scientific article; zbMATH DE number 2043548 (Why is no real title available?)
- scientific article; zbMATH DE number 1615229 (Why is no real title available?)
- Theory and practice of second-order rewriting: foundation, evolution, and SOL
- Nominal rewriting
- Nominal confluence tool
- Normal higher-order termination
- Decreasing diagrams and relative termination
- Infinitary combinatory reduction systems
- scientific article; zbMATH DE number 7340567 (Why is no real title available?)
- A Proof of Finite Family Developments for Higher-Order Rewriting Using a Prefix Property
- Shallow confluence of conditional term rewriting systems
- Superposition for higher-order logic
- The variable containment problem
- Size-based termination of higher-order rewriting
- Expression reduction systems with patterns
- A new connective in natural deduction, and its application to quantum computing
- Unifying sets and programs via dependent types
- Antimirov and Mosses’s Rewrite System Revisited
- scientific article; zbMATH DE number 512772 (Why is no real title available?)
- Processes, Terms and Cycles: Steps on the Road to Infinity
- n-level rewriting systems
- Perpetuality and uniform normalization in orthogonal rewrite systems
- scientific article; zbMATH DE number 1615230 (Why is no real title available?)
- Pure pattern calculus à la de Bruijn
- A restricted form of higher-order rewriting applied to an HDL semantics
- scientific article; zbMATH DE number 2043525 (Why is no real title available?)
- scientific article; zbMATH DE number 1552533 (Why is no real title available?)
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
- scientific article; zbMATH DE number 1405629 (Why is no real title available?)
- Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
- Confluence by critical pair analysis revisited
- Contextual Natural Deduction
- Pushing the frontiers of combining rewrite systems farther outwards
- Superposition with lambdas
- Checking overlaps of nominal rewriting rules
- scientific article; zbMATH DE number 1942460 (Why is no real title available?)
- Higher-order narrowing with convergent systems
- Superposition with lambdas
- scientific article; zbMATH DE number 7559275 (Why is no real title available?)
- Confluence Competition 2015
- On the termination of Russell's description elimination algorithm
- Development closed critical pairs
- Capture-avoiding substitution as a nominal algebra
- Higher-order substitutions
- On proving confluence modulo equivalence for Constraint Handling Rules
- Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding
- Soundness and completeness proofs by coinductive methods
- Algebraic coherent confluence and higher globular Kleene algebras
- Rewriting, and equational unification: the higher-order cases
- Cut elimination, substitution and normalisation
- scientific article; zbMATH DE number 2043524 (Why is no real title available?)
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)
