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.


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


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