cl-banner

Generalized and Formalized Uncurrying

Christian Sternagel and René Thiemann

Proceedings of the 8th International Symposium on Frontiers of Combining Systems (FroCoS 2011), Lecture Notes in Artificial Intelligence 6989, pp. 243 – 258, 2011.

Abstract

Uncurrying is a termination technique for applicative term rewrite systems. During our formalization of uncurrying in the theorem prover Isabelle, we detected a gap in the original pen-and-paper proof which cannot directly be filled without further preconditions. Our final formalization does not demand additional preconditions, and generalizes the existing techniques since it allows to uncurry non-applicative term rewrite systems. Furthermore, we provide new results on uncurrying for relative termination and for dependency pairs.

 

  PDF |    doi:10.1007/978-3-642-24364-6_17  |  © Springer

BibTeX 

@inproceedings{CSRT-FroCoS11,
author = "Christian Sternagel and Ren{\'e} Thiemann",
title = "Generalized and Formalized Uncurrying",
booktitle = "Proceedings of the 8th International Symposium on Frontiers of Combining Systems",
series = "Lecture Notes in Artificial Intelligence",
volume = 6989,
pages = "243--258",
publisher = "Springer-Verlag",
year = 2011
}
Nach oben scrollen