Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

Termination of dependently typed rewrite rules

Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-01239083
Contributor : Jean-Pierre Jouannaud Connect in order to contact the contributor
Submitted on : Monday, December 7, 2015 - 1:45:33 PM
Last modification on : Saturday, June 25, 2022 - 10:18:28 PM
Long-term archiving on: : Saturday, April 29, 2017 - 10:07:29 AM

File

TLCA.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Jean-Pierre Jouannaud, Jian-Qi Li. Termination of dependently typed rewrite rules. Proc. TLCA 2015, Jul 2015, Varsaw, Poland. ⟨10.4230/LIPIcs.TLCA.2015.x⟩. ⟨hal-01239083⟩

Share

Metrics

Record views

135

Files downloads

79