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: 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. 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 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 Workshop 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 Theses and Reports 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 Other 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)