@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}
}
@article {Baggi09,
	title = {An Ontology-based System for Semantic Filtering of XML Data},
	journal = {Electronic Notes in Theoretical Computer Science},
	volume = {235},
	year = {2009},
	pages = {19{\textendash}33},
	publisher = {Elsevier Science Publishers B. V.},
	address = {Amsterdam, The Netherlands, The Netherlands},
	abstract = {In this paper, we describe a system, written in Haskell, for the ontology-based approximate filtering of XML data. Basically, it allows one to extract relevant data as well as to exclude useless and misleading contents from an XML document. The system provides a declarative language one can use to define XML patterns and ontology queries to express syntactic as well as semantic filtering criteria. The system can be used through a Web application which is endowed with a user-friendly graphical interface. Finally, we provide some meaningful examples which show the usefulness of the implemented filtering methodology.},
	keywords = {Haskell, Ontology-based Approximate Filter, XML},
	issn = {1571-0661},
	doi = {http://dx.doi.org/10.1016/j.entcs.2009.03.003},
	author = {Michele Baggi}
}
@proceedings {BBF09,
	title = {Quantitative Pathway Logic for Computational Biology},
	journal = {Computational Methods in Systems Biology, 7th International Conference, CMSB 2009},
	number = {5688},
	year = {2009},
	pages = {68{\textendash}82},
	publisher = {Springer},
	abstract = {This paper presents an extension of Pathway Logic, called Quantitative Pathway Logic (QPL), which allows one to reason about quantitative aspects of biological processes, such as element concentrations and reactions kinetics. Besides, it supports the modeling of inhibitors, that is, chemicals which may block a given reaction whenever their concentration exceeds a certain threshold. QPL models can be specified and directly simulated using rewriting logic or can be translated into Discrete Functional Petri Nets (DFPN) which are a subclass of Hybrid Functional Petri Nets in which only discrete transitions are allowed. Under some constraints over the anonymous variables appearing in the QPL models, the transformation between the two computational models is shown to preserve computations. By using the DFPN representation our models can be graphically visualized and simulated by means of well known tools (e.g. Cell Illustrator); moreover standard Petri net analyses (e.g. topological analysis,  forward/backward reachability, etc.) may be performed on the net model.
An executable framework for QPL and for the translation of QPL models into DFPNs has been implemented using the rewriting-based language Maude. We have tested this system on several examples},
	keywords = {Bioinformatics, Petri nets, Quantitative Pathway Logic, Rewriting Logic},
	author = {Michele Baggi and Demis Ballis and Moreno Falaschi}
}
@proceedings {BB08,
	title = {A Lazy Implementation of a Language for Approximate Filtering of XML Documents},
	journal = {Proceedings of the 16th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2007)},
	volume = {216},
	year = {2008},
	pages = {93{\textendash}109},
	publisher = {Elsevier},
	abstract = {In this  paper, we introduce a system, written in Haskell, for filtering information from  XML data.
Essentially, the system implements a simple declarative language which allows one to extract relevant data
as well as to exclude useless and misleading contents from an XML document by matching patterns against XML
documents.

The matching mechanism employes a cost-based pattern transformation algorithm which
searches for patterns in an approximate way (i.e. modulo renaming, insertion, and deletion of XML items)
and ranks the results w.r.t. their cost.
In order to  improve efficiency, the implementation uses sophisticated indexing techniques
and exploits laziness to automatically avoid the construction of unnecessary data structures.

We analyzed both the expressiveness of our filtering language and the performance of the system
using the well known XMark benchmark suite.},
	keywords = {Approximate Filtering of XML, PHIL},
	author = {Michele Baggi and Demis Ballis}
}
@proceedings {ABBF08,
	title = {Semantic Verification of Web System Contents},
	journal = {ER 2008 Workshops (WISM 2008)},
	volume = {5232},
	year = {2008},
	pages = {437{\textendash}446},
	publisher = {Springer},
	abstract = {In this paper, we present a rule-based
specification language to define and automatically check semantic as
well as syntactic constraints over the informative content of a Web
system. The language is inspired by the GVERDI language and
significantly extends it by integrating ontology reasoning into the
specification rules and by adding new syntactic constructs.  The
resulting language  increases the expressiveness of the original one
and enables a more sophisticated treatment of the semantic
information related to the contents of the Web system.},
	keywords = {Description logic, OWL, Semantic Verification, Web Site Verification},
	author = {Maria Alpuente and Michele Baggi and Demis Ballis and Moreno Falaschi}
}
@proceedings {BBF08,
	title = {XML Semantic Filtering via Ontology Reasoning},
	journal = {3rd International Conference on Internet and Web Applications and Services, ICIW 2008},
	year = {2008},
	pages = {482{\textendash}487},
	publisher = {IEEE Computer Society},
	abstract = {In this paper, we present an extension of PHIL, a declarative language
for filtering information from XML data. The proposed approach allows us to extract relevant data as well as to exclude useless and
misleading contents from an XML document.
Essentially, it combines ontology reasoning with an approximate pattern-matching engine which searches for patterns in a flexible way (i.e. modulo
renaming, insertion, and deletion of XML items) and ranks the
results w.r.t. their cost. 
The filtering process is guided by the syntax as well as the semantics of the XML documents, since it relies on both the document structure and the ontological information to which the document is related.
Such information is retrieved by querying (possibly remote) ontology reasoners.
Ontology reasoning capabilities are integrated into  the filtering language via an adapted version of the DIG interface, which is a standard framework for describing description logic systems. Our extension to the DIG interface allows one to deal with non-ground ontology queries.  },
	keywords = {Approximate Filtering of XML, Description logic, DIG, OWL, PHIL, Semantic Filtering},
	author = {Michele Baggi and Demis Ballis and Moreno Falaschi}
}
