EN FR

Contact

pierre.courtieu@cnam.fr

Position

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.

• official page of the SYS team
• useful links for members of the team (french only)
• My lab page
• seminars of the SYS team

Besides

• I have been (sept 1st 2014-august 31st 2016) in the Gallium team (now Cambium) at INRIA.
• I have been for 6 month in team Proval at LRI, from 1er october 2012 to march 2013

Research

I am mostly interested in formal proof techniques and inparticular the proof of programs. In particular using Coq.

• My phd intro (french) tries to introduce the domain to non logicians.
• My course document on proof of progams
• Publications
• Coq

Current financed projects

• ANR Générique SAPPORO(2019-CE25-0005-1)
  Job and internship offers
  • MODEL VALIDATION FOR LUMINOUS ROBOTS details may be prolonged as PhD
  • CERTIFICATION OF ALGORITHMS FOR (NON-EUCLIDEAN) GEOMETRY details may be prolonged as PhD
  • PROOF AUTOMATION IN GRAPHS AND SWARMS details may be prolonged as PhD
  • RANDOMIZED PROTOCOLS AND THEIR CERTIFICATION details may be prolonged as PhD

Closed financed projects

• ÎdF-Digitéo PACTOLE
• ANR PARAL-ITP,
• Une sémantique formelle de SPARK en Coq (contrat AdaCore 2013-2014)
• ANR blanc A3PAT,
• ANR ARA CompCert
• ANR SESUR SCALP.

Teaching (french only)

Informations pratiques

• Plan du Cnam
• Accéder au Cnam
• Programmer ses inscription au CNAM - mode d’emploi du site du CNAM

cours

• DIU EIL

  • Calendrier session 1
  • moodle

• NFA031

• NFA035

• Master M2IF – option Automated Deduction, and opening to Distributed Algorithms”

  • Slides
  • Tutoriel coq

• Master SEMS

  • Page du master SEMS

• ENSIIE Transparents de Calculabilité:

  • compressés
  • non compressés
  • complet (avec overlays)

Software

• Some emacs stuff
• Une calculette à bande
• inout.{h,c} une librairie C d’entrée sortie simplifiées pour les débutants.

Coq libraries

• 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.