Teaching
2018
TYPES 2018 Summer School - Introduction to Dependent Type Theory
See the dedicated web page.
2013-2018
MPRI 2.7.2 - Proof Assistants
2013-2014
Voir la page du cours.
2013-2014
Proof assistants
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
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
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
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
Initiation to Unix, shell programming, Python programming and
various tools, including editors and RCS.
The Functionnal Approach to Algorithmics
Introduction to functionnal programming and the basics of
algorithmics. The course focused on recursive functions and
simple algebraic datatypes.
Languages and Software Engineering
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
- 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
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.