Raphaël Cauderlier

From sept. 2016 to sept. 2018 I was a postdoc at Irif in team Modélisation et Vérification. I was 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). I am now working at Nomadic Labs.

Contact

Name Raphaël Cauderlier
Mail raphael.cauderlier@nomadic-labs.com

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.

Teaching

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.

Software

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.

Publications

See also dblp.

Conference

Workshop

Theses and Reports

Other