@proceedings {ABBF11,
	title = {Completeness of Unfolding for Rewriting Logic Theories},
	journal = {12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2010},
	year = {2010},
	pages = {116{\textendash}123},
	publisher = {IEEE Computer Society Press},
	abstract = {Many transformation systems for program optimization, program synthesis, and program specialization are based on fold/unfold transformations. In this paper, we investigate the semantic properties of a narrowing-based unfolding transformation that is useful to transform rewriting logic theories. We also present a transformation methodology that is able to determine whether an unfolding transformation step would cause incompleteness and avoid this problem by completing the transformed rewrite theory with suitable extra rules. More precisely, our methodology identifies the sources of incompleteness and derives a set of rules that are added to the transformed rewrite theory in order to preserve the semantics of the original theory.},
	keywords = {Program Transformation, Rewriting Logic, Unfolding},
	author = {Maria Alpuente and Michele Baggi and Demis Ballis and Moreno Falaschi}
}
@proceedings {ABBF10,
	title = {A Fold/Unfold Transformation Framework for Rewrite Theories Extended to CCT},
	journal = {ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2010},
	year = {2010},
	pages = {43{\textendash}52},
	publisher = {Springer},
	abstract = {Many transformation systems for program optimization, program synthesis, and program specialization are based on fold/unfold transformations. In this paper, we present a  fold/unfold-based transformation framework for rewriting logic theories which is based on narrowing. For the best of our knowledge, this is the first fold/unfold transformation framework which allows one to deal with  functions, rules, equations, sorts,  and algebraic laws (such as commutativity and associativity).
We provide correctness results for the transformation system w.r.t. the semantics of ground reducts.
Moreover, we show how our transformation technique can be naturally
applied to implement a Code Carrying Theory (CCT) system.
CCT is an approach for securing delivery of code from a producer to a consumer
where only a certificate (usually in the form of assertions and proofs)
is transmitted from the producer to the consumer who can check its validity and
then extract executable code from it. Within our framework, the certificate
consists of a sequence of transformation steps which can be applied to
a given consumer specification in order to automatically synthesize  safe
code in agreement with the original requirements. 
We also provide an implementation of  the program transformation framework
in the high-performance, rewriting logic language Maude which, by means of
an experimental evaluation of the system,
highlights the potentiality of our approach.},
	keywords = {CCT, Fold/Unfold Transformations, Program Transformation, Rewriting Logic},
	author = {Maria Alpuente and Michele Baggi and Demis Ballis and Moreno Falaschi}
}
@inbook {ABF10,
	title = {Transformation and Debugging of Functional Logic Programs},
	booktitle = {25 Years GULP 2010},
	series = {Lecture Notes in Computer Science},
	year = {2010},
	pages = {271{\textendash}299},
	publisher = {Springer},
	organization = {Springer},
	chapter = {Transformation and Debugging of Functional Logic Programs},
	abstract = {The Italian contribution to 
functional-logic programming has been significant and influential in a number of areas of semantics, and semantics-based program manipulation techniques.
We survey selected topics, with a particular  regard to debugging and 
transformation techniques. These results as usual depend on the
narrowing strategy which is adopted and on the properties satisfied
by the considered programs. In this paper, we restrict ourselves to first-order  functional-logic languages without non-deterministic functions.
We start by describing some basic classical transformation techniques,
namely folding and unfolding.
Then, we recall the
narrowing-driven partial evaluation, which is the first generic algorithm for 
the specialization of functional logic   programs. 
Regarding debugging,
we describe a goal-independent approach to automatic diagnosis and correction 
which applies the immediate consequence operator modeling computed answers
to the diagnosis of bugs in functional logic programs.
A companion bug-correction  program synthesis methodology is 
described that attempts to correct the erroneous
components of the wrong code.},
	keywords = {Debugging, Fold/Unfold Transformations, Functional-logic Programming, Program Transformation},
	author = {Maria Alpuente and Demis Ballis and Moreno Falaschi}
}
@proceedings {ABCF03,
	title = {Correction of Functional Logic Programs},
	journal = {Programming Languages and Systems, 12th European Symposium on Programming, ESOP 2003},
	volume = {2618},
	year = {2003},
	pages = {54{\textendash}68},
	publisher = {Springer},
	abstract = {We propose a new methodology for synthesizing correct
functional logic programs.  We aim to create an integrated development
environment in which it is possible to debug a program and correct
it automatically. We start from a declarative diagnoser that we have developed
previously which allows us
to identify wrong  program rules w.r.t. an intended specification.
Then a bug-correction, program synthesis methodology tries
to correct the erroneous components of the wrong code.
We propose a hybrid, top-down  (unfolding-based)
as well as bottom-up (induction-based), approach
for the automatic correction of functional logic programs
which is driven by a set of evidence examples which are automatically
produced as an outcome by the diagnoser.
The resulting program is proven to be correct and complete
w.r.t. the considered example sets.
Finally, we also provide a prototypical implementation
which we use for an experimental
evaluation of our system.
},
	keywords = {Debugging, Functional-logic Programming, program correction, Program Transformation, Unfolding},
	author = {Maria Alpuente and Demis Ballis and F. Correa and Moreno Falaschi}
}
