My current main research interests concern computation and
deduction by rewriting.
I intend to contribute to the
semantical, logical and practical design of iPPE (integrated
Program and Proof Environment) where the duality between
computation and deduction is better understood and used, and
where rewriting techniques play a fundamental role from theory
to practice.
Applications concerns safe programs as well
as transformation processes for the web and rule based
languages.
- A first goal consists in the study of the semantical and logical aspects of the typed rewriting calculus. Because it offers sophisticated matching capabilities at the level of objects and types, this framework appears to have the potential to integrate uniformly computation and deduction and therefore to be an excellent candidate to backup iPPEs.
- Second, the development of proof techniques in first and higher-order logics, based on the main paradigm of Deduction Modulo. This should lead to the uniform integration of automated and interactive deduction with a particular emphasis on the safe use of decision procedures.
- Then, the design of such rewrite based environments, based on the Formal Islands, where expressivity and efficiency are reach by the appropriate use of compilation and re-usable implementation techniques.
PROTHEO is the project I am currently working on and where we develop the ELAN and TOM languages and systems.
