Français English
Studies
Here one can find
a complete description of the courses I followed during my studies at
University from L1 to M1 (in French).

September 2009 to August 2013 : Ph.D. of Computer Science
Formal proofs with SMT
The automatic tools used to decide the Satisfiability Modulo
Theories (SMT) are particularly successful and are largely
used to solve problems coming from software verification or
computer security.
We aim at give these high performing systems to Coq users. Coq is an
interactive theorem prover of which proof system is generalist.
First we will focus on the algorithms that are critical to establish
the validity of the results coming from a SMTsolver. Then we will
implement them and validate them in Coq. We hope to obtain an
automatic proof tactic that will be powerful.
Development: SMTCoq
Publications and talks: see the
Research webpage.
Supervisors: Benjamin
Werner
and Germain
Faure
Place : Laboratoire
d'informatique de Polytechnique,
INRIA TypiCal team

February to July 2009 : Research internship in Computer Science
Importing HOLLight proofs into Coq
During this internship, I developed an interface to automatically
import HOL Light's theorems into Coq.
Subject
(in French)
Development: HOLLIGHTCOQ
Internship
report (in French)
Internship
presentation (in French)
Publications and talks: see the
Research webpage
Supervisor: Benjamin
Werner
Place: Laboratoire
d'Informatique de Polytechnique,
INRIA TypiCal team

20082009 : M2 of Science majoring in Fundamental Computer
Science at the MPRI of Paris, France

Programming languages semantics

Proof systems

Proof assistants
I implemented in Coq a simplytyped λcalculus with
polarities. The surroundings were
the proof
assistants project.
Here is the source code:
the definitions,
the decidability
proof,
the correction
proof (not finished yet). Here is
a report
(in French) explaining the code.

Linear logic

Constraint programming
I realised a GNUProlog program that generates of nontransitive
dice set, according to
the constraint
programming project.

Functional programming and type systems

Automatic deduction
I realised a termination checker for rewriting systems, in
OCaml. It implements the subterm termination criterion. The
surroundings were
the
automatic deduction programming project.
The source code is
available here,
and there is
a report
(in French) explaining it.

Linguistic modelling using logical and computational tools

Synchronous systems
I studied the technical
report A
clocked denotational semantic for LucidSynchrone in Coq by
Sylvain Boulmé, Grégoire Hamon and Marc Pouzet. I translated
their implementation from Coq v.6.3.1 to Coq v.8.1.
The original sources are
available here.
Please ask me in order to get the translated sources.
I made
a report
that explains this article and my work (in French).

Categories and λcalculi
I studied the
article Intuitionistic
model constructions and normalization proofs by Thierry
Coquand and Peter Dybjer.
I implemented all the systems they present, as well as strong
normalisation proofs, in
Coq: Gödel
system
T, propositional
calculus, Brouwer
ordinals.
Finally, I presented this article; here are
my slides
(in French).

June to August, 2008 : Research internship in Computer Science
Substitutions for simplytyped λcalculus
The category of simply typed λterms in Agda
In the beginning of my trainee, I studied substitutions in simply
typed λcalculus. I proved they form a category which has finite
products, using the proof
assistant Agda.
The originality of the proof resides in the chosen approach for
λcalculus and substitutions:
 we consider only typed terms, and we do not previously
define pure λcalculus;
 we prefer parallel substitutions.
Development:
Notes: see the Research webpage

During the second part of my internship, I studied hereditary
substitutions in the simply typed λcalculus. Please refer to
the dedicated webpage.
Development: HSUBST
Publications and talks: see
the Research webpage
Internship report
Internship
presentation (in French)
Supervisor: Thorsten
Altenkirch
Place: Functional Programming team of
the School of Computer
Science at the University
of Nottingham

20072008 : M1 of Science majoring in Fundamental Computer Science
at the ENS of Lyon, France

Algebraic calculus
I studied the article Probabilistic
computation of the Smith normal form of a sparse integer matrix
by Mark Giesbrecht.
I made a report
that explains this article (in French), and a twentyminutes talk
related to this article, where one can find the slides here
(in French).

Euclidian networks
I studied the article Lattices
with many cycles are dense by Mårten Trolin.
I made a report
that explains this article (in French), and a twentyminutes talk
related to this article, where one can find the slides here
(in French).

Highspeed matrix computation
I studied the article Limitations of the PlayStation
3 for High Performance Cluster Computing by Alfredo Buttari, Jack
Dongarra and Jakub Kurzak.
I made a report
that explains this article (in French), and a twentyminutes talk
related to this article, where one can find the slides here (in
French).

Parallelism semantics
I studied the article Service
combinators for farming virtual machines by K. Bhargavan, A. D.
Gordon and I. Narasamdya.
I made a report
that explains this article (in French), and a twentyminutes talk
related to this article, where one can find the slides here (in French).

Proof theory
I studied the article Computational
types from a logical perspective by P.N. Benton, G.M. Bierman and
V.C.V. De Paiva.
I made a report
that explains this article (in French), and a twentyminutes talk
related to this article, where one can find the slides here (in French).

Graphs
I studied the article Resolution
limit in community detection by Santo Fortunato and Marc
Barthélemy.
I made a twentyminutes talk related to this article, where one can
find the slides here (in
French).
I also studied the article Efficient
data structure for sparse network representation by Jörkki
Hyvönen, Jari Saramäki and Kimmo Kaski.
I made a twentyminutes talk related to this article, where one can
find the slides here (in French).

Parallel algorithms

Probabilities

Arithmetic algorithms

Computer assisted proofs

Compilation

Image

June and July, 2007 : Internship in Computer Science
Pseudohaptic manipulation of 2D objects
During this internship, I implemented a software measuring the
pressure exerted on a tabletop. By coupling it with a visual
feedback, I implemented a pseudohaptic system giving a weight
sensation to 2D virtual objects. This system was evaluated in order
to measure the table sensibility and the effect felt by the
users.
Internship
report (in French)
Supervisors: Sabine
Coquillart and Renaud Blanch
Place: INRIA
RhôneAlpes and Laboratoire
d'Informatique de Grenoble

20062007 : Bachelor of Science majoring in Fundamental Computer Science
at the ENS of Lyon, France

Programming

Algorithms

Calculability

Architectures, operating systems, networks

Project
Last update: 12/01/14