Germain FAURE INRIA Saclay Ile-de-France

---

For the time being, I am a full-time junior researcher in the TypiCal team, located at the Computer Science Lab of the Ecole Polytechnique (LIX). I am working on the verification of proofs produced by automatic prover inside skeptical proof assistants like the Coq system. I am a member of

• the ANR project Psi about proof search control in interaction with domain specific methods.
• the ANR project DeCert about the design of an architecture for the combination of decision procedures.

I was the coordinator the INRIA ARC Corias about the conception of proof assistants based on superdeduction modulo. Previsouly, I began to study computer science seriously at the ENS Lyon. One year and a half later, I moved to Uppsala (Sweden). I studied for the master of programmation at Paris 7. I am awarded a PhD degree from Nancy University about the Rho-Calculus under the supervision H.Cirstea and C.Kirchner. I also work with A.Miquel. Then I did a one year post-doc with R.Nieuwenhuis contributing to SAT/SMT solvers.

---

During my past and present research I have been studying:

• SAT-solvers and their implementations
• SAT Modulo the Theory of Linear Arithmetic and the use of Operational Research solvers in this context
• SAT Modulo the Theory of Bit Vectors
  
• Some lambda-calculi (the lambda-calculus and the parallel lambda-calculus).
• Pattern-calculi especially the rho-calculus and their syntactical properties (such as the confluence).
• Higher-order matching.
• Models for the parallel lambda-calculus and for the rho-calculus.
• Calculi with explicit substitution and explicit matching.
• Interactions nets.
• Typed equality and subtyping.

---