Raphaël Cauderlier

Tel 06 10 25 32 03
email 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.


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).



PhD manuscript

Author: root

Created: 2016-07-28 jeu. 16:42

Emacs 24.4.1 (Org mode 8.2.10)