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.

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:
  • type-theoretic proof assistants, in particular the Coq proof assistant,
  • tactic languages;
• 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.

See also dblp.

• Raphaël Cauderlier, Tactics and certificates in Meta Dedukti, (code: dktactics dktransfer), ITP 2018
• Raphaël Cauderlier, Mihaela Sighireanu, A Verified Implementation of the Bounded List Container (slides, code), TACAS 2018
• Raphaël Cauderlier, Catherine Dubois, FoCaLiZe and Dedukti to the Rescue for Proof Interoperability (slides, code), ITP 2017
• Raphaël Cauderlier, Catherine Dubois, ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti (slides, code), ICTAC 2016 (tool paper)
• Raphaël Cauderlier, Catherine Dubois, Object and Subtyping in the λΠ-calculus modulo (slides, code), TYPES 2014 (post-proceedings)
• H. J. Sander Bruggink, Raphaël Cauderlier, Mathias Hülsbusch, and Barbara König, Conditional Reactive Systems, FSTTCS 2011

• Bruno Bernardo, Raphaël Cauderlier, Basile Pesin, Julien Tesson, Albert, an intermediate smart-contract language for the Tezos blockchain, WTSC 2020
• Bruno Bernardo, Raphaël Cauderlier, Zhenlei Hu, Basile Pesin, Julien Tesson, Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts, FMBC 2019
• Raphaël Cauderlier, A rewrite system for proof constructivization (slides, code), LFMTP 2016
• Guillaume Bury, Raphaël Cauderlier, Pierre Halmagrand, Implementing Polymorphism in Zenon, IWILL 2015
• Ali Assaf, Raphaël Cauderlier, Mixing HOL and Coq in Dedukti, PxTP 2015
• Raphaël Cauderlier, Pierre Halmagrand, Checking Zenon Modulo proofs in Dedukti, PxTP 2015

• Object-oriented mechanisms for interoperability between proof systems (slides), PhD Thesis, 2016
• Traits orientés objet en λΠ-calcul modulo, Compilation de FoCaLize vers Dedukti (fr), Master Thesis, 2012
• Certifying in Isabelle an automata-based reachability algorithm for Pushdown systems, Internship Report, 2011
• Comparing two category-theory based logics for graphs, Internship Report, 2010

• Ali Assaf, Raphaël Cauderlier, and Ronan Saillard, Dedukti, un vérificateur de preuves universel (fr), Journée Nationales 2013, CIEL, AFADL, GDR GPL (poster session)
• Raphaël Cauderlier, A Rewrite System for Elimination of the Functional Extensionality and Univalence Axioms (unpublished)
• Raphaël Cauderlier, Strong Equivalence and the univalence axiom (unpublished)