License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TLCA.2015.257
URN: urn:nbn:de:0030-drops-51684
URL: http://drops.dagstuhl.de/opus/volltexte/2015/5168/
Go to the corresponding LIPIcs Volume Portal


Jouannaud, Jean-Pierre ; Li, Jianqi

Termination of Dependently Typed Rewrite Rules

pdf-format:
23.pdf (0.5 MB)


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.

BibTeX - Entry

@InProceedings{jouannaud_et_al:LIPIcs:2015:5168,
  author =	{Jean-Pierre Jouannaud and Jianqi Li},
  title =	{{Termination of Dependently Typed Rewrite Rules}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{257--272},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Thorsten Altenkirch},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5168},
  URN =		{urn:nbn:de:0030-drops-51684},
  doi =		{10.4230/LIPIcs.TLCA.2015.257},
  annote =	{Keywords: rewriting, dependent types, strong normalization, path orderings}
}

Keywords: rewriting, dependent types, strong normalization, path orderings
Seminar: 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
Issue Date: 2015
Date of publication: 12.06.2015


DROPS-Home | Fulltext Search | Imprint Published by LZI