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
@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
}