Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility (Q896904): Difference between revisions

@@ Property / describes a project that uses @@
+Agda
@@ Property / describes a project that uses: Agda / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Matita
@@ Property / describes a project that uses: Matita / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Automath
@@ Property / describes a project that uses: Automath / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W1791042548
@@ Property / OpenAlex ID: W1791042548 / rank @@
+Normal rank
@@ Property / arXiv ID @@
+.00649
@@ Property / arXiv ID: 1509.00649 / rank @@
+Normal rank
@@ Property / cites work @@
+Termination checking with types
@@ Property / cites work: Termination checking with types / rank @@
+Normal rank
@@ Property / cites work @@
+Explicit substitutions
@@ Property / cites work: Explicit substitutions / rank @@
+Normal rank
@@ Property / cites work @@
+Termination of term rewriting using dependency pairs
+Normal rank
@@ Property / cites work @@
+The Matita Interactive Theorem Prover
@@ Property / cites work: The Matita Interactive Theorem Prover / rank @@
+Normal rank
@@ Property / cites work @@
+The lambda calculus. Its syntax and semantics. Rev. ed.
+Normal rank
@@ Property / cites work @@
+Q4023900
@@ Property / cites work: Q4023900 / rank @@
+Normal rank
@@ Property / cites work @@
+A Brief Overview of Agda – A Functional Language with Dependent Types
+Normal rank
@@ Property / cites work @@
+Modularity of strong normalization in the   algebraic-λ-cube
+Normal rank
@@ Property / cites work @@
+Type-based termination of recursive definitions
@@ Property / cites work: Type-based termination of recursive definitions / rank @@
+Normal rank
@@ Property / cites work @@
+Q4938611
@@ Property / cites work: Q4938611 / rank @@
+Normal rank
@@ Property / cites work @@
+Inductive-data-type systems
@@ Property / cites work: Inductive-data-type systems / rank @@
+Normal rank
@@ Property / cites work @@
+The Computability Path Ordering: The End of a Quest
+Normal rank
@@ Property / cites work @@
+The computability path ordering
@@ Property / cites work: The computability path ordering / rank @@
+Normal rank
@@ Property / cites work @@
+Relating Higher-order and First-order Rewriting
@@ Property / cites work: Relating Higher-order and First-order Rewriting / rank @@
+Normal rank
@@ Property / cites work @@
+Q2723890
@@ Property / cites work: Q2723890 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4447247
@@ Property / cites work: Q4447247 / rank @@
+Normal rank
@@ Property / cites work @@
+Rewriting Techniques and Applications
@@ Property / cites work: Rewriting Techniques and Applications / rank @@
+Normal rank
@@ Property / cites work @@
+Definitions by rewriting in the Calculus of Constructions
+Normal rank
@@ Property / cites work @@
+Computability Closure: Ten Years Later
@@ Property / cites work: Computability Closure: Ten Years Later / rank @@
+Normal rank
@@ Property / cites work @@
+Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems
+Normal rank
@@ Property / cites work @@
+On the Relation between Sized-Types Based Termination and Semantic Labelling
+Normal rank
@@ Property / cites work @@
+Q4205074
@@ Property / cites work: Q4205074 / rank @@
+Normal rank
@@ Property / cites work @@
+Polymorphic rewriting conserves algebraic strong normalization
+Normal rank
@@ Property / cites work @@
+Constructive versions of Tarski's fixed point theorems
+Normal rank
@@ Property / cites work @@
+Q5565113
@@ Property / cites work: Q5565113 / rank @@
+Normal rank
@@ Property / cites work @@
+The calculus of constructions
@@ Property / cites work: The calculus of constructions / rank @@
+Normal rank
@@ Property / cites work @@
+Combining algebraic rewriting, extensional lambda calculi, and fixpoints
+Normal rank
@@ Property / cites work @@
+The rewriting calculus - part I
@@ Property / cites work: The rewriting calculus - part I / rank @@
+Normal rank
@@ Property / cites work @@
+The rewriting calculus - part II
@@ Property / cites work: The rewriting calculus - part II / rank @@
+Normal rank
@@ Property / cites work @@
+Q5667469
@@ Property / cites work: Q5667469 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3857730
@@ Property / cites work: Q3857730 / rank @@
+Normal rank
@@ Property / cites work @@
+Orderings for term-rewriting systems
@@ Property / cites work: Orderings for term-rewriting systems / rank @@
+Normal rank
@@ Property / cites work @@
+Q4385532
@@ Property / cites work: Q4385532 / rank @@
+Normal rank
@@ Property / cites work @@
+Proving termination with multiset orderings
@@ Property / cites work: Proving termination with multiset orderings / rank @@
+Normal rank
@@ Property / cites work @@
+Adding algebraic rewriting to the untyped lambda calculus (extended abstract)
+Normal rank
@@ Property / cites work @@
+Adding algebraic rewriting to the untyped lambda calculus
+Normal rank
@@ Property / cites work @@
+Q4222854
@@ Property / cites work: Q4222854 / rank @@
+Normal rank
@@ Property / cites work @@
+Polynomial Interpretations for Higher-Order Rewriting
+Normal rank
@@ Property / cites work @@
+Q3922646
@@ Property / cites work: Q3922646 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4219036
@@ Property / cites work: Q4219036 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5625124
@@ Property / cites work: Q5625124 / rank @@
+Normal rank
@@ Property / cites work @@
+Processes, Terms and Cycles: Steps on the Road to Infinity
+Normal rank
@@ Property / cites work @@
+ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
+Normal rank
@@ Property / cites work @@
+Q3997237
@@ Property / cites work: Q3997237 / rank @@
+Normal rank
@@ Property / cites work @@
+Generalized sufficient conditions for modular termination of rewriting
+Normal rank
@@ Property / cites work @@
+An initial algebra approach to term rewriting systems with variable binders
+Normal rank
@@ Property / cites work @@
+Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
+Normal rank
@@ Property / cites work @@
+Rewriting Techniques and Applications
@@ Property / cites work: Rewriting Techniques and Applications / rank @@
+Normal rank
@@ Property / cites work @@
+Completion of a Set of Rules Modulo a Set of Equations
+Normal rank
@@ Property / cites work @@
+First-class patterns
@@ Property / cites work: First-class patterns / rank @@
+Normal rank
@@ Property / cites work @@
+Q3336736
@@ Property / cites work: Q3336736 / rank @@
+Normal rank
@@ Property / cites work @@
+Abstract data type systems
@@ Property / cites work: Abstract data type systems / rank @@
+Normal rank
@@ Property / cites work @@
+Higher-Order Orderings for Normal Rewriting
@@ Property / cites work: Higher-Order Orderings for Normal Rewriting / rank @@
+Normal rank
@@ Property / cites work @@
+Polymorphic higher-order recursive path orderings
@@ Property / cites work: Polymorphic higher-order recursive path orderings / rank @@
+Normal rank
@@ Property / cites work @@
+Q5581665
@@ Property / cites work: Q5581665 / rank @@
+Normal rank
@@ Property / cites work @@
+The Theory of Calculi with Explicit Substitutions Revisited
+Normal rank
@@ Property / cites work @@
+Q3356291
@@ Property / cites work: Q3356291 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3918095
@@ Property / cites work: Q3918095 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2740996
@@ Property / cites work: Q2740996 / rank @@
+Normal rank
@@ Property / cites work @@
+Lambda calculus with patterns
@@ Property / cites work: Lambda calculus with patterns / rank @@
+Normal rank
@@ Property / cites work @@
+Combinatory reduction systems: Introduction and survey
+Normal rank
@@ Property / cites work @@
+Higher Order   Matching is Undecidable
@@ Property / cites work: Higher Order Matching is Undecidable / rank @@
+Normal rank
@@ Property / cites work @@
+Termination of combined (rewrite and λ-calculus) systems
+Normal rank
@@ Property / cites work @@
+Q4720069
@@ Property / cites work: Q4720069 / rank @@
+Normal rank
@@ Property / cites work @@
+A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
+Normal rank
@@ Property / cites work @@
+Higher-order rewrite systems and their confluence
@@ Property / cites work: Higher-order rewrite systems and their confluence / rank @@
+Normal rank
@@ Property / cites work @@
+Proofs of strong normalisation for second order classical natural deduction
+Normal rank
@@ Property / cites work @@
+Constructing recursion operators in intuitionistic type theory
+Normal rank
@@ Property / cites work @@
+Proofs of the normalization and Church-Rosser theorems for the typed \(\lambda\)-calculus
+Normal rank
@@ Property / cites work @@
+Complete Sets of Reductions for Some Equational Theories
+Normal rank
@@ Property / cites work @@
+Linear unification of higher-order patterns
@@ Property / cites work: Linear unification of higher-order patterns / rank @@
+Normal rank
@@ Property / cites work @@
+On the Stability by Union of Reducibility Candidates
+Normal rank
@@ Property / cites work @@
+Functionals defined by recursion
@@ Property / cites work: Functionals defined by recursion / rank @@
+Normal rank
@@ Property / cites work @@
+The typed lambda-calculus is not elementary recursive
+Normal rank
@@ Property / cites work @@
+Decidability of higher-order matching
@@ Property / cites work: Decidability of higher-order matching / rank @@
+Normal rank
@@ Property / cites work @@
+A Characterization of Medial as Rewriting Rule
@@ Property / cites work: A Characterization of Medial as Rewriting Rule / rank @@
+Normal rank
@@ Property / cites work @@
+Q3682462
@@ Property / cites work: Q3682462 / rank @@
+Normal rank
@@ Property / cites work @@
+Intensional interpretations of functionals of finite type I
+Normal rank
@@ Property / cites work @@
+Q4093416
@@ Property / cites work: Q4093416 / rank @@
+Normal rank
@@ Property / cites work @@
+Parallel reductions in \(\lambda\)-calculus
@@ Property / cites work: Parallel reductions in \(\lambda\)-calculus / rank @@
+Normal rank
@@ Property / cites work @@
+A lattice-theoretical fixpoint theorem and its applications
+Normal rank
@@ Property / cites work @@
+Q4799892
@@ Property / cites work: Q4799892 / rank @@
+Normal rank
@@ Property / cites work @@
+Counterexamples to termination for the direct sum of term rewriting systems
+Normal rank
@@ Property / cites work @@
+Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
+Normal rank
@@ Property / cites work @@
+On Computable Numbers, with an Application to the Entscheidungsproblem
+Normal rank
@@ Property / cites work @@
+On Computable Numbers, with an Application to the Entscheidungsproblem. A Correction
+Normal rank
@@ Property / cites work @@
+Q3856127
@@ Property / cites work: Q3856127 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3127078
@@ Property / cites work: Q3127078 / rank @@
+Normal rank
@@ Property / cites work @@
+Semantic types
@@ Property / cites work: Semantic types / rank @@
+Normal rank
@@ Property / cites work @@
+Dependent types for program termination verification
+Normal rank
@@ Property / cites work @@
+Q4847000
@@ Property / cites work: Q4847000 / rank @@
+Normal rank