scientific article; zbMATH DE number 7559275

DOI10.4230/LIPIcs.FSCD.2019.9MaRDI QIDQ5089009

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

Publication date: 18 July 2022

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

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

terminationdependent typeshigher-order rewritingdependency pairs

Mathematics Subject Classification ID

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

Related Items (3)

A modular construction of type theories ⋮ Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules ⋮ Unnamed Item

Cites Work

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

This page was built for publication: