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
(70)- Perpetuality and uniform normalization in orthogonal rewrite systems
- scientific article; zbMATH DE number 7559275 (Why is no real title available?)
- Confluence by critical pair analysis revisited
- Superposition with lambdas
- Inductive-data-type systems
- Unifying sets and programs via dependent types
- Nominal confluence tool
- Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding
- scientific article; zbMATH DE number 1615230 (Why is no real title available?)
- scientific article; zbMATH DE number 2043525 (Why is no real title available?)
- scientific article; zbMATH DE number 1552533 (Why is no real title available?)
- scientific article; zbMATH DE number 1405629 (Why is no real title available?)
- scientific article; zbMATH DE number 1942460 (Why is no real title available?)
- Normal higher-order termination
- Pushing the frontiers of combining rewrite systems farther outwards
- Formally verified animation for RoboChart using interaction trees
- Infinitary combinatory reduction systems
- Algebraic coherent confluence and higher globular Kleene algebras
- A linear proof language for second-order intuitionistic linear logic
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
- The variable containment problem
- Processes, Terms and Cycles: Steps on the Road to Infinity
- Rewriting, and equational unification: the higher-order cases
- scientific article; zbMATH DE number 7340567 (Why is no real title available?)
- Decreasing diagrams and relative termination
- Contextual Natural Deduction
- Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules
- scientific article; zbMATH DE number 2043548 (Why is no real title available?)
- Expression reduction systems with patterns
- Capture-avoiding substitution as a nominal algebra
- Size-based termination of higher-order rewriting
- On the termination of Russell's description elimination algorithm
- A linear linear lambda-calculus
- Superposition with lambdas
- Checking overlaps of nominal rewriting rules
- Higher-order substitutions
- Superposition for higher-order logic
- Tableaux for automated reasoning in dependently-typed higher-order logic
- 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
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
- scientific article; zbMATH DE number 512772 (Why is no real title available?)
- How to prove decidability of equational theories with second-order computation analyser SOL
- Sharing proofs with predicative theories through universe-polymorphic elaboration
- A characterization of basic feasible functionals through higher-order rewriting and tuple interpretations
- Nominal rewriting
- A new connective in natural deduction, and its application to quantum computing
- Sort-based confluence criteria for non-left-linear higher-order rewriting
- The computability path order for beta-eta-normal higher-order rewriting
- Confluence Competition 2015
- Impredicativity, cumulativity and product covariance in the logical framework dedukti
- n-level rewriting systems
- Shallow confluence of conditional term rewriting systems
- scientific article; zbMATH DE number 176122 (Why is no real title available?)
- An algebraic extension of intuitionistic linear logic: the \(\mathcal{L}_!^{\mathcal{S}}\)-calculus and its categorical model
- Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs
- Higher-order superposition for dependent types
- scientific article; zbMATH DE number 1615229 (Why is no real title available?)
- Higher-order narrowing with convergent systems
- scientific article; zbMATH DE number 2043524 (Why is no real title available?)
- On proving confluence modulo equivalence for Constraint Handling Rules
- Cut elimination, substitution and normalisation
- Antimirov and Mosses’s Rewrite System Revisited
- An execution model for RICE
- A restricted form of higher-order rewriting applied to an HDL semantics
- Development closed critical pairs
- Closed nominal rewriting and efficiently computable nominal algebra equality
- Finite family developments
- Pure pattern calculus à la de Bruijn
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)
