Horațiu Cîrstea

University of Lorraine & LORIA

Abstract

Rewriting is a formalism widely used in computer science and mathematical logic. The classical formalism has been extended, in the context of functional languages, with an order over the rules and, in the context of rewrite based languages, with the negation over patterns. We have proposed a concise and clear algorithm computing the difference over patterns which can be used to define generic encodings of constructor term rewriting systems with negation and order into classical term rewriting systems. As a direct consequence, established methods used for term rewriting systems can be applied to analyze properties of the extended systems. The approach can also be seen as a generic compiler which targets any language providing basic pattern matching primitives.

The formalism provides also a new method for deciding if a set of patterns subsumes a given pattern and thus, for checking the completeness of a set of patterns, the presence of useless patterns, or the absence of some patterns. The latter is particularly useful when one wants to verify that some patterns are absent from the result of a particular transformation and several extensions have been proposed to statically verify the absence of specified patterns from the reachable terms of constructor based term rewriting systems.

Short Bio

Horațiu Cîrstea obtained his Master’s Degree in Computer Science from the University Politehnica of Bucharest and after an one year fellowship at Oxford University he went on to obtain his PhD in Computer Science from t he University Henri Poincaré in 2000. Since September 2011, he is Professor at the University of Lorraine. His main research interests include the theoretical foundations of rewriting and logic and their practical applications to the specification and verification of computer systems.

He introduced the rewriting calculus and studied in collaboration with several scientists the properties, the extensions and the applications of this calculus. He’s been involved in the development of the rewrite based languages Elan and TOM and on their application for the description and validation of various concrete systems. More recently, he has been working on extensions of programming and specification languages, with the aim of improving their expressiveness and safety.