Abstract
The rewriting calculus is a minimal framework embedding lambda calculus and term rewriting systems that allows abstraction on variables and patterns. The rewriting calculus features higher-order functions (from the lambda calculus) and pattern matching (from term rewriting systems). In this paper, we study extensively the decidability of type inference in the second-order rewriting calculus à la Curry.

URL:
http://rewerse.net/publications/rewerse-publications.html#REWERSE-RP-2006-016

BibTeX:

@inproceedings{REWERSE-RP-2006-016,
	author = {Horatiu Cirstea and Claude Kirchner and Luigi Liquori and Benjamin Wack},
	title = {Decidable Type Inference for the Polymorphic Rewriting Calculus},
	booktitle = {Proceedings of 17èmes Journées Francophones des Langages Applicatifs , Pauillac, France (28th--31st January 2006)},
	year = {2006},
	organization = {INRIA},
	url = {http://rewerse.net/publications/rewerse-publications.html#REWERSE-RP-2006-016}
}