Termination of Dependently Typed Rewrite Rules

Jouannaud, Jean-Pierre; Li, Jianqi

doi:10.4230/LIPIcs.TLCA.2015.257

Document

Termination of Dependently Typed Rewrite Rules

Authors Jean-Pierre Jouannaud, Jianqi Li

Part of: Volume: 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: International Conference on Typed Lambda Calculi and Applications (TLCA)
License: Creative Commons Attribution 3.0 Unported license
Publication Date: 2015-06-15

PDF

File

PDF

LIPIcs.TLCA.2015.257.pdf

Filesize: 0.51 MB
16 pages

Document Identifiers

DOI: 10.4230/LIPIcs.TLCA.2015.257
URN: urn:nbn:de:0030-drops-51684

Subject Classification

Keywords

rewriting
dependent types
strong normalization
path orderings

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

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.

Cite As Get BibTex

Jean-Pierre Jouannaud and Jianqi Li. Termination of Dependently Typed Rewrite Rules. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 257-272, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.TLCA.2015.257

Author Details

Jean-Pierre Jouannaud

Jianqi Li

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail