@article {150,
	title = {A Condensed Goal-Independent Fixpoint Semantics Modeling the Small-Step Behavior of Rewriting},
	year = {2013},
	month = {02/2013},
	type = {Technical Report},
	abstract = {It is well known that it does not exist a condensed goal-independent bottom-up semantics for the full class of term rewriting systems. This kind of semantics is essential for the development of efficacious semantics- based program manipulation tools (e.g. automatic program analyzers and debuggers).

The big-step rewriting semantics that is most commonly considered in functional programming is the set of values/normal forms that the program is able to compute for any input expression. Such a big-step semantics is unnecessarily oversized, as it contains many {\textquotedblleft}semantically useless{\textquotedblright} elements that can be retrieved from a smaller set of terms.

In this paper we present a novel condensed narrowing-like semantics that contains the minimal information which is needed to describe compo- sitionally all possible rewritings. We provide its goal-dependent top-down definition and, more importantly, an equivalent goal-independent bottom- up fixpoint characterization.
We prove soundness and completeness w.r.t. the small-step behavior of rewriting for the full class of term rewriting systems.

This semantics constitutes the first step for the development of a condensed goal-independent bottom-up fixpoint semantics fully abstract w.r.t. the big-step behavior of rewriting (an ongoing work).},
	keywords = {property-oriented specifications, semantics-based inference methods, TRS},
	author = {Marco Comini and Luca Torella}
}
@proceedings {BacciCFV12,
	title = {The additional difficulties for the automatic synthesis of specifications posed by logic features in functional-logic languages},
	journal = {Technical Communications of the 28th International Conference on Logic Programming (ICLP 2012)},
	volume = {17},
	year = {2012},
	pages = {144-153},
	address = {Budapest, Hungary},
	abstract = {This paper discusses on the additional issues for the automatic inference of algebraic property-oriented specifications which arises because of interaction between laziness and logical variables in lazy functional logic languages.
We present an inference technique that overcomes these issues for the first-order fragment of the lazy functional logic language Curry. Our technique statically infers from the source code of a Curry program a specification which consists of a set of equations relating (nested) operation calls
that have the same behavior. Our proposal is a (glass-box) semantics-based inference method which can guarantee, to some extent, the correctness of the inferred specification, differently from other (black-box) approaches based on testing techniques.},
	keywords = {Curry, property-oriented specifications, semantics-based inference methods},
	isbn = {978-3-939897-43-9},
	issn = {978-3-939897-43-9},
	author = {Giovanni Bacci and Marco Comini and Marco Antonio Feli{\'u} and Alicia Villanueva},
	editor = {Agostino Dovier and V. Santos Costa}
}
