@proceedings {149,
	title = {TRSynth: a Tool for Automatic Inference of Term Equivalence in Left-linear Term Rewriting Systems},
	journal = {ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation (PEPM{\textquoteright}13)},
	year = {2013},
	abstract = {In this paper we propose a parametric technique to automatically infer algebraic property-oriented specifications from Term Rewriting Systems. Namely, given the source code of a TRS we infer a specification which consists of a set of most general equations relating terms that rewrite, for all possible instantiations, to the same set of normal forms.

The semantic-based inference method that we propose can cope with non-constructor-based TRSs, and considers non-ground terms. Particular emphasis is posed to avoid the generation of {\textquotedblleft}redundant{\textquotedblright} equations that can be a logical consequence of other ones.

To experiment on the validity of our proposal we have considered an instance of the method employing a novel (condensed) semantics for left-linear TRSs and we have implemented a {\textquotedblleft}proof of concept{\textquotedblright} prototype in Haskell which is available online.},
	author = {Marco Comini and Luca Torella}
}
