Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
From MaRDI portal
Publication:896904
DOI10.1016/j.tcs.2015.07.045zbMath1332.68103arXiv1509.00649OpenAlexW1791042548MaRDI QIDQ896904
Publication date: 15 December 2015
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1509.00649
typesrewriting\(\lambda\)-calculusterminationGirard's reducibilitymatching modulo \(\beta\eta\)patterns à la Millerrewriting modulo
Related Items
Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding, Size-based termination of higher-order rewriting, How to prove decidability of equational theories with second-order computation analyser SOL, Unnamed Item, Unnamed Item, Theory and practice of second-order rewriting: foundation, evolution, and SOL
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Orderings for term-rewriting systems
- The lambda calculus. Its syntax and semantics. Rev. ed.
- An initial algebra approach to term rewriting systems with variable binders
- Lambda calculus with patterns
- Constructing recursion operators in intuitionistic type theory
- Counterexamples to termination for the direct sum of term rewriting systems
- The calculus of constructions
- Higher-order rewrite systems and their confluence
- Polymorphic rewriting conserves algebraic strong normalization
- Adding algebraic rewriting to the untyped lambda calculus
- Proofs of the normalization and Church-Rosser theorems for the typed \(\lambda\)-calculus
- The typed lambda-calculus is not elementary recursive
- Constructive versions of Tarski's fixed point theorems
- Combinatory reduction systems: Introduction and survey
- Generalized sufficient conditions for modular termination of rewriting
- Combining algebraic rewriting, extensional lambda calculi, and fixpoints
- Abstract data type systems
- Dependent types for program termination verification
- Termination of term rewriting using dependency pairs
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- Functionals defined by recursion
- A lattice-theoretical fixpoint theorem and its applications
- The rewriting calculus - part I
- The rewriting calculus - part II
- A Brief Overview of Agda – A Functional Language with Dependent Types
- The computability path ordering
- ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
- Relating Higher-order and First-order Rewriting
- Decidability of higher-order matching
- Semantic types
- Higher-Order Orderings for Normal Rewriting
- The Computability Path Ordering: The End of a Quest
- Polymorphic higher-order recursive path orderings
- The Theory of Calculi with Explicit Substitutions Revisited
- Computability Closure: Ten Years Later
- First-class patterns
- On the Relation between Sized-Types Based Termination and Semantic Labelling
- Completion of a Set of Rules Modulo a Set of Equations
- Proving termination with multiset orderings
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Complete Sets of Reductions for Some Equational Theories
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- Modularity of strong normalization in the algebraic-λ-cube
- Proofs of strong normalisation for second order classical natural deduction
- Type-based termination of recursive definitions
- Definitions by rewriting in the Calculus of Constructions
- Termination checking with types
- Higher Order Matching is Undecidable
- Explicit substitutions
- Linear unification of higher-order patterns
- Adding algebraic rewriting to the untyped lambda calculus (extended abstract)
- Polynomial Interpretations for Higher-Order Rewriting
- The Matita Interactive Theorem Prover
- Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems
- A Characterization of Medial as Rewriting Rule
- Intensional interpretations of functionals of finite type I
- On the Stability by Union of Reducibility Candidates
- On Computable Numbers, with an Application to the Entscheidungsproblem
- On Computable Numbers, with an Application to the Entscheidungsproblem. A Correction
- Termination of combined (rewrite and λ-calculus) systems
- Processes, Terms and Cycles: Steps on the Road to Infinity
- Rewriting Techniques and Applications
- Rewriting Techniques and Applications
- Parallel reductions in \(\lambda\)-calculus
- Inductive-data-type systems
