I am currently maître de conférence (associate professor) at CNAM, in the SYS of Cédric laboratory. I am currently the (rotating) team leader of SYS.
Besides
I am mostly interested in formal proof techniques and inparticular the proof of programs. In particular using Coq.
Stage secondes
DIU EIL
NFA031
NFA035
Master M2IF – option Automated Deduction, and opening to Distributed Algorithms”
Master SEMS
ENSIIE Transparents de Calculabilité:
LybHyps (author: Pierre Courtieu) A library for hypothesis manipulations in Coq. Written in Ltac, it allows to apply tactics to all new hypothesis after a tactic, including a sophisticated (and customizable) autonaming heuristics.
Sparkformal (Zhi Zang, Pierre Courtieu) A semantic for a subset of the Spark programing language. The archive also include the textual semantic in Z format of Spark written in 1983 (author Ian O’Neill and William March).
SparkCompcert (Pierre Courtieu) Spark frontend for CompCert (work in progress), based on Sparkformal above is the most up to date. Based on and dependening on the semantic above.
loglangcoq (Pierre Courtieu, Julien Forest, Olivier Pons) A Coq development on first order propositional logic and programming language semantics. Proofs on the tableaux method, and completness results of natural deduction are also included. coqdoc here.
PMachine (Tristan Crolard, Maria-Virginia Aponte, Julia Lawall, Pierre Courtieu) A Coq development formalising a part of the P-machine for a toy language à la SPARK-ADa using the parametricity plugin (Marc Lasson) proving the equivalence between two implementations of the procedure frame stack. Nested procedures in part of the difficulty here, together with the absence of closure.
ProofGeneral ProofGeneral, emacs mode for Coq (David Aspinal, Paul Steckler, Erik Martin-Dorel, Pierre Courtieu, Hendriks Tews).
Pactole Coq Framework for proving distributed protocols for autonomous robots. Some non trivial protocoles together with impossibility proofs.