Teaching
2018
TYPES 2018 Summer School - Introduction to Dependent Type Theory
See the dedicated web page.
2013-2018
MPRI 2.7.2 - Proof Assistants
Master 2 Research Introduction to Proof Assistants and in particular Coq's type theory. See the dedicated page.
2013-2014
Master 2 Pro
Voir la page du cours.
2013-2014
Proof assistants
MPRI - Level 2 course
My first lecture (jan 27th) was about record types and modular and generic development in Coq. Solutions to the lecture exercises and the Fibonacci derivation are available. My second lecture (feb 3rd) was about a practical introduction to (co-)inductive types in Coq. Solutions to the lecture exercises, including the rest of the previous lecture exercises on monadic programming are available. My last lecture on feb 24th was about dependently-typed programming and a bit of models of Type Theory. The solutions to exercises are available.
2012-2013
Proof assistants
MPRI - Level 2 course
My first lecture was about modular and generic development in Coq. Corrections are available for the matrices and the monad exercices. My (and the course's) last lecture was about dependently-typed programming (exercises, correction).
I used to teach at university Paris XI Orsay.
2007-2008
The Functionnal Approach to Algorithmics
Second year of University, first semester
20 hours of directed works, 15 hours of practical works
Introduction to functionnal programming and the basics of algorithmics. The focus of the course is on types, recursive functions, algebraic datatypes and modular programming this time.
2006-2007
Administration of the practical works network
Equivalent to 20 hours of directed works
Administration of the computer network used by students. The architecture is a Linux server and diskless terminals, it is mostly maintainance and setting up new servers.
Unix project
Third year of University, first semester
40 hours of practical works (two groups)
Initiation to Unix, shell programming, Python programming and various tools, including editors and RCS.
The Functionnal Approach to Algorithmics
Second year of University, first semester
24 hours of practical works
Introduction to functionnal programming and the basics of algorithmics. The course focused on recursive functions and simple algebraic datatypes.
Languages and Software Engineering
Second year of University, second semester
14 hours of practical works
Introduction to software engineering methods using a medium-size project and paired programming. The subject was the development of an Arkanoid clone in OCaml, from the game model to the interaction loop excluding the graphical library.
2005-2006
Introduction to Computer Science
First year of University, first semester
20 hours of directed works
  • Integer, floating-point representations. Simple cryptographic codes.
  • Basic processor architecture and assembler program interpretation.
  • Manipulation of numbers, arrays and strings with conditionals, loops in restricted C. Same thing in assembler.
Compilation project
Fourth year of University, first semester
40 hours of practical works
Compilation of a pascal-like language with pattern-matching using OCaml. Includes sum types declarations, arrays, references, functions and procedures. The project is done in three phases: lexing and parsing with
ocamllex
and
ocamlyacc
, typing and code generation for a stack-based virtual machine.
Valid XHTML 1.1! Valid CSS!