@mastersthesis {Bacci11,
	title = {An Abstract Interpretation Framework for Semantics and Diagnosis of Lazy Functional-Logic Languages},
	number = {??},
	year = {2012},
	school = {Universit{\`a} di Udine},
	type = {Ph.D.},
	abstract = {This thesis presents a fixed-point semantics for Curry programs which is fully-abstract with respect to the computed (I/O) behavior. Curry is a declarative language that combines in a seamless way features from functional programming (nested expressions, lazy evaluation, higher-order functions) and logic programming (logical variables, partial data structures, built-in search). Among other proposals, the presented semantics has the following pragmatical features: it is goal-independent, condensed and it is a congruence w.r.t. usage (i.e. unions among modules). We also described an abstract interpretation framework for systematically obtain, from this semantics, several abstract semantics which approximate the (I/O) behavior of a Curry program. These kinds of abstract semantics are particularly suitable for developing efficacious semantics-based program manipulation tools. 
To support this claim some applications as been provided: a static analyzer for groundness dependencies, an abstract debugging/diagnosis method, and an automatic method for synthesizing algebraic property-oriented specifications. Moreover, by means of a program transformation into a Curry semantic-equivalent version, these tools also apply to first order purely functional Haskell programs.},
	keywords = {Abstract Interpretation, Curry, Functional-logic Programming},
	author = {Giovanni Bacci}
}
@proceedings {BacciCFV12-ICLP,
	title = {The additional difficulties for the automatic synthesis of specifications posed by logic features in functional-logic languages},
	journal = {ICLP (Technical Communications)},
	volume = {To appear},
	year = {2012},
	publisher = {Schloss Dagstuhl - Leibniz-Zentrum Fuer Informatik},
	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.},
	author = {Giovanni Bacci and Marco Comini and Marco Antonio Feli{\'u} and Alicia Villanueva}
}
@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}
}
@proceedings {BacciCFV12,
	title = {Automatic Synthesis of Specifications for First Order Curry Programs},
	journal = {Proceedings of the 14th symposium on Principles and practice of declarative programming},
	year = {2012},
	pages = {25{\textendash}34},
	publisher = {ACM},
	address = {New York, NY, USA},
	abstract = {This paper presents a technique to automatically infer algebraic property-oriented specifications from first-order Curry programs. Curry is a lazy functional logic language and the interaction between laziness and logical variables raises some additional difficulties with respect to other proposals for functional languages. 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. We propose a (glass-box) semantic-based inference method which relies on a fully-abstract (condensed) semantics for achieving, to some extent, the correctness of the inferred specification, differently from other (black-box) approaches based on testing techniques.},
	keywords = {Curry, property-oriented specifications, semantic-based inference methods},
	isbn = {978-1-4503-1522-7},
	doi = {10.1145/2370776.2370781},
	url = {http://doi.acm.org/10.1145/2370776.2370781},
	author = {Giovanni Bacci and Marco Comini and Marco Antonio Feli{\'u} and Alicia Villanueva}
}
@proceedings {BacciC10absdiag,
	title = {Abstract Diagnosis of First Order Functional Logic Programs},
	journal = {Logic-based Program Synthesis and Transformation, 20th International Symposium},
	volume = {6564},
	year = {2011},
	pages = {215--233},
	publisher = {Springer-Verlag},
	address = {Berlin},
	abstract = {We present a generic scheme for the abstract debugging of functional logic programs. We associate to programs a semantics based on a (continuous) immediate consequence operator, P[[R]], which models correctly the powerful features of modern functional logic languages (non-deterministic, non-strict functions defined by non-confluent programs and call-time choice behaviour). Then, we develop an effective debugging methodology which is based on abstract interpretation: by approximating the intended specification of the semantics of R we derive a finitely terminating bottom-up diagnosis method, which can be used statically. Our debugging framework does not require the user to provide error symptoms in advance and is applicable with partial specifications and even partial programs.},
	author = {Giovanni Bacci and Marco Comini},
	editor = {Maria Alpuente}
}
@proceedings {BacciCFV11,
	title = {Automatic Synthesis of Specifications for Curry Programs},
	journal = {Logic-based Program Synthesis and Transformation, 21th International Symposium {\textendash} Pre-Proceedings},
	year = {2011},
	note = {To appear},
	publisher = {Springer-Verlag},
	address = {Odense, Denmark},
	abstract = {This extended abstract presents a technique to automatically infer specifications from Curry programs. Program specifications (in particular, automatically derived specifications) have been used for program verification, understanding, documentation, service discovering or testing. Our technique, statically infers from the source code of a Curry program a specification which consists of a set of semantic properties that the program operations satisfy. These properties are given by means of equations relating (nested) operation calls that have the same behavior. Our method relies on the semantics of [<a href="http://flit.dimi.uniud.it/?q=biblio/baccic10conc">1</a>] for achieving, to some extent, the correctness of the inferred specification, as opposed to other similar tools based on testing.
In this paper, we present the main ideas of the approach emphasizing the difficulties addressed for the case of the Curry language.},
	keywords = {Abstract Interpretation, Algebraic-oriented Specification, Curry},
	author = {Giovanni Bacci and Marco Comini and Marco Antonio Feli{\'u} and Alicia Villanueva}
}
@proceedings {BacciC10absdiag,
	title = {Abstract Diagnosis of First Order Functional Logic Programs},
	journal = {Logic-Based Program Synthesis and Transformation {\textendash} 20th International Symposium {\textendash} Pre-Proceedings},
	volume = {10-14},
	year = {2010},
	pages = {58{\textendash}72},
	edition = {20},
	address = {Hagenberg, Austria},
	abstract = {We present a generic scheme for the abstract debugging of functional-logic programs. We associate to our programs a semantics based on a (continuous) immediate consequence operator, P[[R]], which models correctly the typical cogent features of modern functional-logic languages (non-deterministic, non-strict functions defined by non-confluent programs and call-time choice behaviour). Then, we develop an effective debugging methodology which is based on abstract interpretation: by approximating the intended specification of the semantics of R we derive a finitely terminating bottom-up diagnosis method, which can be used statically. Our debugging framework does not require the user to either provide error symptoms in advance or answer questions concerning program correctness.},
	keywords = {Abstract Diagnosis, Debugging, Declarative Diagnosis, Functional-logic Programming},
	author = {Giovanni Bacci and Marco Comini},
	editor = {Maria Alpuente}
}
@article {BacciC10conc,
	title = {A Compact Goal-Independent Bottom-Up Fixpoint Modeling of the Behaviour of First Order Curry},
	number = {6/2010},
	year = {2010},
	publisher = {Dipartimento di Matematica e Informatica, Universit{\`a} di Udine},
	abstract = {This work is motivated by the fact that a {\textquotedblleft}compact{\textquotedblright} semantics for functional logic languages, which is essential for the development of efficacious semantics-based program manipulation tools (e.g. automatic program analyzers and debuggers), does not exist. The operational or the rewriting logic semantics that are most commonly considered in func- tional logic are unnecessarily oversized, as they contains many {\textquotedblleft}semantically useless{\textquotedblright} elements that can be retrieved from a smaller set of {\textquotedblleft}basic{\textquotedblright} elements. Therefore, in this article, we present a compressed, goal-independent bottom-up fixpoint semantics that is correct and minimal w.r.t. answers computed for Curry expressions.
We believe that the compactness of the semantics makes it particularly suitable for applications. Actually, our semantics can be finite whereas the big-step semantics is generally not, and even when both semantics are infinite, the fixpoint computation of our semantics produces fewer elements at each step.},
	keywords = {Abstract Interpretation, call-time choice semantics, Functional-logic Programming},
	url = {http://www.dimi.uniud.it/comini/Papers/},
	author = {Giovanni Bacci and Marco Comini}
}
