@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}
}
