Size-based termination of higher-order rewriting
From MaRDI portal
Publication:4577817
DOI10.1017/S0956796818000072zbMath1476.68048arXiv1802.06603OpenAlexW2963645437WikidataQ129977183 ScholiaQ129977183MaRDI QIDQ4577817
Publication date: 3 August 2018
Published in: Journal of Functional Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1802.06603
Related Items (2)
Uses Software
Cites Work
- Intensional interpretations of functionals of finite type I
- The Principal Type-Scheme of an Object in Combinatory Logic
- A system of abstract constructive ordinals
- Typed Lambda Calculi and Applications
- Types for Proofs and Programs
- New Computational Paradigms
- On the Stability by Union of Reducibility Candidates
- Termination by absence of infinite chains of dependency pairs
- An ordinal calculus for proving termination in term rewriting
- Semi-continuous Sized Types and Termination
- Rewriting Techniques and Applications
- The consistency of arithmetics
- An ordinal measure based procedure for termination of functions
- Inductive-data-type systems
- Calculating sized types
- 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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Quasi-interpretations. A way to control resources
- Termination of rewriting systems by polynomial interpretations and its implementation
- Orderings for term-rewriting systems
- Proofs by induction in equational theories with constructors
- Mechanically proving termination using polynomial interpretations
- An initial algebra approach to term rewriting systems with variable binders
- Mechanizing and improving dependency pairs
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
- Type inference with subtypes
- Matrix interpretations for proving termination of term rewriting
- A domain model characterising strong normalisation
- Proving termination of normalization functions for conditional expressions
- Higher-order rewrite systems and their confluence
- A note on simplification orderings
- LCF considered as a programming language
- A theory of type polymorphism in programming
- Minimax algebra
- Constructive versions of Tarski's fixed point theorems
- Testing positiveness of polynomials
- Combinatory reduction systems: Introduction and survey
- Termination of nested and mutually recursive algorithms
- Indexed types
- Dependent types for program termination verification
- Simplifying subtyping constraints: a theory
- Modular termination proofs for rewriting using dependency pairs
- Termination of term rewriting using dependency pairs
- SAT solving for termination proofs with recursive path orders and dependency pairs
- Enhancing dependency pair method using strong computability in simply-typed term rewriting
- Automating the dependency pair method
- The size-change principle and dependency pairs for termination of term rewriting
- Inductive types and type constraints in the second-order lambda calculus
- On theories with a combinatorial definition of 'equivalence'
- A lattice-theoretical fixpoint theorem and its applications
- A predicative analysis of structural recursion
- Derivation Lengths Classification of G\"odel's T Extending Howard's Assignment
- Guarded recursive datatype constructors
- Universality of quantum Turing machines with deterministic control
- A Monotonic Higher-Order Semantic Path Ordering
- Harnessing First Order Termination Provers Using Higher Order Dependency Pairs
- The computability path ordering
- ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
- Improved Matrix Interpretation
- Complexity Bounds for Ordinal-Based Termination
- Union of Reducibility Candidates for Orthogonal Constructor Rewriting
- Call-by-value Termination in the Untyped lambda-calculus
- Root-Labeling
- Predictive Labeling
- Type-Based Termination with Sized Products
- Polymorphic higher-order recursive path orderings
- Signature Extensions Preserve Termination
- SAT Solving for Termination Analysis with Polynomial Interpretations
- Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems
- On the Values of Reducibility Candidates
- On the Relation between Sized-Types Based Termination and Semantic Labelling
- Proving termination with multiset orderings
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- Coherence of subsumption, minimum typing and type-checking in F ≤
- Modularity of strong normalization in the algebraic-λ-cube
- How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study
- Type-based termination of recursive definitions
- Transforming termination by self-labelling
- Definitions by rewriting in the Calculus of Constructions
- Termination checking with types
- On Strong Normalization of the Calculus of Constructions with Type-Based Termination
- Towards a domain theory for termination proofs
- The size-change principle for program termination
- Polynomials over the reals in proofs of termination : from theory to practice
- Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems
- CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
- Higher Order Dependency Pairs for Algebraic Functional Systems
- Closing the Gap Between Runtime Complexity and Polytime Computability.
- Computer Science Logic
- The Size-Change Termination Principle for Constructor Based Languages
- A proof of strong normalisation using domain theory
- A SAT-Based Approach to Size Change Termination with Global Ranking Functions
- Search Techniques for Rational Polynomial Orders
- A Machine-Oriented Logic Based on the Resolution Principle
This page was built for publication: Size-based termination of higher-order rewriting
