Dependency pairs termination in dependent type theory modulo rewriting

DOI10.4230/LIPICS.FSCD.2019.9MaRDI QIDQ5089009FDOQ5089009

Authors: Frédéric Blanqui, Guillaume Genestier, Olivier Hermant 

Publication date: 18 July 2022

Full work available at URL: https://arxiv.org/abs/1906.11649

Recommendations

• scientific article; zbMATH DE number 1722701
• Termination of dependently typed rewrite rules
• Modular termination proofs for rewriting using dependency pairs
• Term Rewriting and Applications
• Rewriting Techniques and Applications

zbMATH Keywords

dependent typesterminationdependency pairshigher-order rewriting

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of computing (68Qxx)

Cites Work

• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• A framework for defining logics
• Chain-complete posets and directed sets with applications
• Combinatory reduction systems: Introduction and survey
• Termination of term rewriting using dependency pairs
• The size-change principle for program termination
• Title not available (Why is that?)
• Title not available (Why is that?)
• Enhancing dependency pair method using strong computability in simply-typed term rewriting
• Logic for Programming, Artificial Intelligence, and Reasoning
• Tyrolean termination tool: techniques and features
• Mechanizing and improving dependency pairs
• Higher-order rewrite systems and their confluence
• Developing developments
• A general formulation of simultaneous inductive-recursive definitions in type theory
• The size-change principle and dependency pairs for termination of term rewriting
• Definitions by rewriting in the Calculus of Constructions
• Rewriting Techniques and Applications
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
• Programming Languages and Systems
• Size-based termination of higher-order rewriting
• The size-change termination principle for constructor based languages
• Calculating sized types
• Refinement types as higher-order dependency pairs
• Termination of dependently typed rewrite rules

Cited In (5)

• Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules
• Proving confluence in the confluence framework with confident
• Automated Reasoning
• Title not available (Why is that?)
• A modular construction of type theories

This page was built for publication: Dependency pairs termination in dependent type theory modulo rewriting

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5089009)