Contact information

My face

Kappa softwares

Kappa is a domain specific language designed to model protein-protein interaction based on stochastic graph rewrites. I work on 3 axes:

  • Algorithmic&compilation: Efficiency of the interpreter (the simulator)
  • Software ingineering: Interactibility with biologist (User interface and exposure as a python library)
  • Porgraming language for graph inspection (the mixture of proteins)

OCaml expertise

The tezos blockchain code base is in OCaml and Nomadic Labs works on its development with strong concern for formal methods. I'm involved in the release process there.

I take any occasion to write programs in my mother tongue and freelanced to do so on several other occasion.

Inductive in Coq

I was PhD student in Université Paris Diderot in PPS lab suppervised by Hugo Herbelin about dependently typed programming inside the Coq proof assistant.

I've kept as archeology the webpage (in French) about my defense.

During my PhD, I spent nearly all my time, hacking Coq.

Training in theoretical computer science

I have been student at the École normale supérieure de Lyon in the Computer Science Department for two years. Then, I studied at the MPRI. My interships dealt about:

Terminaison en PI-Calcul (PLUME @ LIP ENS Lyon) under the responsibility of Romain Demangeon and Sebastien Briais.
Equality over lambda-terms with list primitives (MSP @ Computer and Informations Sciences departement Strathclyde university) under the supervision of Conor McBride.
Dependent pattern-matching in Coq (Πr2 @ INRIA Rocquencourt) with Hugo Herbelin.

Teaching material in French

TD algorithmique M1 et TP initiation à la programmation L1
2011/2012 - 2012/2013
TD d'initiation à l'algorithmique pour la licence de BioInfo et Cours/TP d'initialtion aux systèmes d'exploitation L1
TP programmation fonctionnelle L3, TP analyse lexicale et syntaxique L3 et TD Compilation M1
TP de Caml Light en MPSI
Computationnal biology Master