===== Raphaël Cauderlier =====

From sept. 2016 to sept. 2018 I was a postdoc at [[:index|Irif]] in team [[equipes:verif:index|Modélisation et Vérification]]. I was working inside the [[http://vecolib.imag.fr|Vecolib ANR project]] on verification of imperative container libraries. Before that, I did a [[https://who.rocq.inria.fr/Raphael.Cauderlier/|PhD]] on interoperability of proof systems at Inria, LSV and CNAM. Here is {{ :users:cauderlier:cv.pdf |my resume}} ({{ :users:cauderlier:cv_fr.pdf |in french}}). I am now working at [[https://nomadic-labs.com|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:
    * type-theoretic proof assistants, in particular [[https://coq.inria.fr|the Coq proof assistant]],
    * tactic languages;
  * logical frameworks: 
    * heuristic axiom elimination,
    * interoperability of proof assistants, in particular in [[http://dedukti.gforge.inria.fr|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:
  * [[http://deducteam.gforge.inria.fr/focalide|Focalide]]: a Dedukti backend for the [[http://focalize.inria.fr|FoCaLiZe]] environment for modular verification of functional programs,
  * [[http://sigmaid.gforge.inria.fr|Sigmaid]]: a translator from an object calculus (the simply-typed ς-calculus) to Dedukti,
  * [[https://gitlab.math.univ-paris-diderot.fr/cauderlier/dklib|Dklib]]: a library defining basic datatypes such as booleans, n-bits numbers, lists and strings in [[http://dedukti.gforge.inria.fr|Dedukti]],
  * [[https://gitlab.math.univ-paris-diderot.fr/cauderlier/dktactics|Dktactics]]: a tactic language for [[http://deducteam.gforge.inria.fr/metadedukti|Meta Dedukti]],
  * [[https://gitlab.math.univ-paris-diderot.fr/cauderlier/dktransfer|Dktransfer]]: a transfer tactic written in Dktactics,
  * [[https://gitlab.math.univ-paris-diderot.fr/cauderlier/math_transfer|MathTransfer]]: a library of transfer theorems written in FoCaLiZe,
  * [[http://deducteam.gforge.inria.fr/sukerujo|Sukerujo]]: syntactic extensions for Dedukti,

I have also contributed to the following tools:
  * [[http://dedukti.gforge.inria.fr|Dedukti]]: a logical framework based on type theory and rewriting,
  * [[http://deducteam.gforge.inria.fr/zenonmodulo|Zenon Modulo]]: a deduction modulo tableaux first-order theorem prover producing Dedukti proofs,
  * [[http://deducteam.gforge.inria.fr/metadedukti|Meta Dedukti]]: a Dedukti to Dedukti translator.

==== Publications ====

See also [[https://dblp.uni-trier.de/pers/hd/c/Cauderlier:Rapha=euml=l|dblp]].

=== Conference ===
  * Raphaël Cauderlier, {{ :users:cauderlier:article_ITP18.pdf |Tactics and certificates in Meta Dedukti}}, (code: [[https://gitlab.math.univ-paris-diderot.fr/cauderlier/dktactics|dktactics]] [[https://gitlab.math.univ-paris-diderot.fr/cauderlier/dktransfer|dktransfer]]), ITP 2018
  * Raphaël Cauderlier, Mihaela Sighireanu, {{ users:cauderlier:article_tacas18.pdf |A Verified Implementation of the Bounded List Container}} ({{ users:cauderlier:slides_tacas18.pdf |slides}}, [[https://drive.google.com/file/d/0B1icXLreOTsqVWxNUFdRU3pxYW8/view?usp=sharing|code]]), TACAS 2018
  * Raphaël Cauderlier, Catherine Dubois, [[https://hal.inria.fr/hal-01592243|FoCaLiZe and Dedukti to the Rescue for Proof Interoperability]] ({{ users:cauderlier:slides_itp17.pdf |slides}}, [[https://gitlab.math.univ-paris-diderot.fr/cauderlier/math_transfer|code]]), ITP 2017
  * Raphaël Cauderlier, Catherine Dubois, [[https://hal.inria.fr/hal-01420638v1|ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti]] ({{ users:cauderlier:slides_ictac.pdf |slides}}, [[http://deducteam.gforge.inria.fr/focalide/index.html|code]]), ICTAC 2016 (tool paper)
  * Raphaël Cauderlier, Catherine Dubois, [[https://hal.inria.fr/hal-01097444|Object and Subtyping in the λΠ-calculus modulo]] ([[https://www.irif.fr/~letouzey/types2014/slides-20.pdf|slides]], [[http://sigmaid.gforge.inria.fr/|code]]), TYPES 2014 (post-proceedings)
  * H. J. Sander Bruggink, Raphaël Cauderlier, Mathias Hülsbusch, and Barbara König, [[http://drops.dagstuhl.de/opus/volltexte/2011/3325|Conditional Reactive Systems]], FSTTCS 2011

=== Workshop ===

  * Bruno Bernardo, Raphaël Cauderlier, Basile Pesin, Julien Tesson, [[https://arxiv.org/abs/2001.02630|Albert, an intermediate smart-contract language for the Tezos blockchain]], WTSC 2020
  * Bruno Bernardo, Raphaël Cauderlier, Zhenlei Hu, Basile Pesin, Julien Tesson, [[https://arxiv.org/abs/1909.08671|Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts]], FMBC 2019
  * Raphaël Cauderlier, [[https://hal.inria.fr/hal-01420634v1|A rewrite system for proof constructivization]] ({{ users:cauderlier:slides_lfmtp16.pdf |slides}}, [[https://gforge.inria.fr/projects/dedukti-constr/|code]]), LFMTP 2016
  * Guillaume Bury, Raphaël Cauderlier, Pierre Halmagrand, [[https://hal.inria.fr/hal-01243593v1|Implementing Polymorphism in Zenon]], IWILL 2015
  * Ali Assaf, Raphaël Cauderlier, [[https://arxiv.org/abs/1507.08721|Mixing HOL and Coq in Dedukti]], PxTP 2015
  * Raphaël Cauderlier, Pierre Halmagrand, [[https://hal.inria.fr/hal-01171360v1|Checking Zenon Modulo proofs in Dedukti]], PxTP 2015

=== Theses and Reports ===

  * [[https://hal.inria.fr/tel-01415945|Object-oriented mechanisms for interoperability between proof systems]] ({{ users:cauderlier:slides_phd.pdf |slides}}), PhD Thesis, 2016
  * {{ :users:cauderlier:rapport_m2.pdf |Traits orientés objet en λΠ-calcul modulo, Compilation de FoCaLize vers Dedukti (fr)}}, Master Thesis, 2012
  * {{ :users:cauderlier:rapport_m1.pdf |Certifying in Isabelle an automata-based reachability algorithm for Pushdown systems}}, Internship Report, 2011
  * {{ :users:cauderlier:rapport_l3.pdf |Comparing two category-theory based logics for graphs}}, Internship Report, 2010

=== Other ===

  * Ali Assaf, Raphaël Cauderlier, and Ronan Saillard, [[http://dedukti.gforge.inria.fr/poster.pdf|Dedukti, un vérificateur de preuves universel (fr)]], Journée Nationales 2013, CIEL, AFADL, GDR GPL (poster session)
  * Raphaël Cauderlier, [[https://gitlab.math.univ-paris-diderot.fr/cauderlier/univalence-elim/blob/master/ua.org|A Rewrite System for Elimination of the Functional Extensionality and Univalence Axioms]] (unpublished)
  * Raphaël Cauderlier, [[https://framagit.org/rafoo/strong_equivalence|Strong Equivalence and the univalence axiom]] (unpublished)