I am a postdoc at Irif in team Modélisation et Vérification. I am working inside the Vecolib ANR project on verification of imperative container libraries. Before that, I did a PhD on interoperability of proof systems at Inria, LSV and CNAM. Here is my resume (in french).


Name Raphaël Cauderlier
Office 4029a
Mail raphael.cauderlier@irif.fr
Phone 06 10 25 32 03

Research Interest

I work in the domain of proof theory. I am interested in the following topics in particular:

  • proof automation:
    • SMT solvers,
    • first-order theorem provers,
    • deduction modulo,
    • induction provers,
    • intuitionistic provers;
  • computer-assisted proof:
  • logical frameworks:
    • heuristic axiom elimination,
    • interoperability of proof assistants, in particular in the Dedukti logical framework,
    • certificate-checking for automatic provers;
  • applications to software verification:
    • operational semantics of functional, object-oriented, and imperative programming languages,
    • interactive proof development of software functional correctness in separation logic,
    • proof automation in separation logic.


I enjoy teaching computer science, both practical topics such as programming, networking, operating systems, and databases and theoretical topics such as logic, λ-calculus, rewriting, semantics of programming languages, software verification, and type theory.


I am the main developer of the following tools and libraries:

  • Focalide: a Dedukti backend for the FoCaLiZe environment for modular verification of functional programs,
  • Sigmaid: a translator from an object calculus (the simply-typed ς-calculus) to Dedukti,
  • Dklib: a library defining basic datatypes such as booleans, n-bits numbers, lists and strings in Dedukti,
  • Dktactics: a tactic language for Meta Dedukti,
  • Dktransfer: a transfer tactic written in Dktactics,
  • MathTransfer: a library of transfer theorems written in FoCaLiZe,
  • Sukerujo: syntactic extensions for Dedukti,

I have also contributed to the following tools:

  • Dedukti: a logical framework based on type theory and rewriting,
  • Zenon Modulo: a deduction modulo tableaux first-order theorem prover producing Dedukti proofs,
  • Meta Dedukti: a Dedukti to Dedukti translator.




Theses and Reports