Raphaël Cauderlier
| Tel | 06 10 25 32 03 |
prenom . nom @inria.fr |
I am a PhD student at LSV, member of Deducteam (Inria) and CPR (Cnam/Cédric). I am working on interoperability of logical systems and on translations of programming languages, in particular object-orientation, to the logical framework Dedukti.
Here is my resume.
Software
I develop the following tools:
- Dklib: Dedukti library defining basic datatypes such as booleans, n-bits numbers, lists and strings.
- Sukerujo: syntactic extension of Dedukti.
- Focalide: backend for the FoCaLiZe compiler producing Sukerujo code.
- Sigmaid: translator from simply-typed ς-calculus to Dedukti.
I have also contributed to the following projects:
- Dedukti: I have developed a parser known as Sukerujo extending Dedukti syntax with notations for natural numbers, strings, records and local definitions.
- Zenon Modulo: I have added Dedukti/Sukerujo as input format and I have implemented a simple type-checking/inference algorithm for ML-like polymorphism.
- Dedukti-interop: I have linked in Dedukti a Coq certification of insertion sort (translated by Coqine) and the HOL definition of natural numbers and ordering (translated by Holide).
Papers
- Raphaël Cauderlier, Catherine Dubois, ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti, ICTAC 2016
- Raphaël Cauderlier, A rewrite system for proof constructivization, LFMTP 2016
- Guillaume Bury, Raphaël Cauderlier, Pierre Halmagrand, Implementing Polymorphism in Zenon, IWILL 2015
- Raphaël Cauderlier, Pierre Halmagrand, Checking Zenon Modulo proofs in Dedukti, PxTP 2015
- Ali Assaf, Raphaël Cauderlier, Mixing HOL and Coq in Dedukti, PxTP 2015
- Raphaël Cauderlier, Catherine Dubois, Object and Subtyping in the λΠ-calculus modulo, TYPES 2014
- Ali Assaf, Raphaël Cauderlier, and Ronan Saillard, Dedukti, un vérificateur de preuves universel (fr), 2013, poster presenting Dedukti and translation tools
- Traits orientés objet en λΠ-calcul modulo, Compilation de FoCaLize vers Dedukti (fr), 2012, master thesis
- Certifying in Isabelle an automata-based reachability algorithm for Pushdown systems, 2011, internship report
- H. J. Sander Bruggink, Raphaël Cauderlier, Mathias Hülsbusch, and Barbara König, Conditional Reactive Systems, FSTTCS 2011
- Comparing two category-theory based logics for graphs, 2010, internship report