2026-07-22T01:18:02Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5168 2024-03-06T10:36:11Z ddc:004 open_access

Termination of Dependently Typed Rewrite Rules Jouannaud, Jean-Pierre Li, Jianqi rewriting dependent types strong normalization path orderings Our interest is in automated termination proofs of higher-order rewrite rules in presence of dependent types modulo a theory T on base types. We first describe an original transformation to a type discipline without type dependencies which preserves non-termination. Since the user must reason on expressions of the transformed language, we then introduce an extension of the computability path ordering CPO for comparing dependently typed expressions named DCPO. Using the previous result, we show that DCPO is a well-founded order, behaving well in practice. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jean-Pierre Jouannaud and Jianqi Li 2015 Is Part Of LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TLCA.2015.257 urn:nbn:de:0030-drops-51684 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.257 eng https://creativecommons.org/licenses/by/3.0/legalcode