Dependency pairs termination in dependent type theory modulo rewriting

DOI10.4230/LIPICS.FSCD.2019.9MaRDI QIDQ5089009zbMATH OpenFDO

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

zbMATH Keywords

dependent typesterminationdependency pairshigher-order rewriting

Mathematics Subject Classification ID

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

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

Cites work

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

Cited in

(5)

• Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules
• Automated Reasoning
• Proving confluence in the confluence framework with confident
• scientific article; zbMATH DE number 7566074 (Why is no real title available?)
• 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)