Français English

Studies

• 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 SMT-solver. 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 HOL-Light 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
  

• 2008-2009 : 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 simply-typed λ-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 GNU-Prolog 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 sub-term 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 Lucid-Synchrone 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 simply-typed λ-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:
    • propositional equality
    • proofs
    Notes: see the Research webpage

  • Decidability of βη-equivalence according to hereditary substitutions

    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

• 2007-2008 : 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 twenty-minutes 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 twenty-minutes talk related to this article, where one can find the slides here (in French).

  • High-speed 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 twenty-minutes 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 twenty-minutes 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 twenty-minutes 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 twenty-minutes 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 twenty-minutes 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

  Pseudo-haptic 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 pseudo-haptic 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ône-Alpes and Laboratoire d'Informatique de Grenoble
  

• 2006-2007 : Bachelor of Science majoring in Fundamental Computer Science at the ENS of Lyon, France

  • Programming

  • Algorithms

  • Calculability

  • Architectures, operating systems, networks

  • Project

  ---

  Home

  Research

  Teaching

  Studies

  Miscellaneous

  Last update: 12/01/14