Section: Dissemination

Teaching - Supervision - Juries

Teaching

• Frédéric Blanqui organized a 7-days school at the Institute of Applied Mechanics and Informatics (IAMA) of the Vietnamese Academy of Sciences and Technology (VAST) at Ho Chi Minh City, Vietnam, from 12 to 19 March 2013. The mornings were dedicated to theoretical lectures introducing basic notions in mathematics and logic for the analysis of computer programs. The afternoons were practical sessions introducing the OCaml programming language and the Coq proof assistant. Lecture notes are given in [17] .

• Vania Joloboff has taught simulation seminars at Shenzhen Institutes of Advanced Technology.

• Licence: Jean-François Monin, Introduction to Interactive Proof of Software, 50 hours, L3, Tsinghua University, China

  This course is expected to attract students in the Formes group via the local PhD program; already one of them (2009) is currently a PhD student of Jean-Pierre Jouannaud, another (2010) in is the PhD track with Gu Ming and 2 others (2010) work with Jean-François Monin and Vania Joloboff.

• Doctorate: Jean-François Monin (organizer and teacher), Coq Summer School, 30 hours, Tsinghua University, China

Supervision

• PhD : Xiaomu Shi, “Certification of an Instruction Set Simulator”, University of Grenoble, July 2013, [14] Jean-François Monin, Vania Joloboff.

• PhD in progress: Kim-Quyen Ly, automated formal verification of termination certificates, October 2011, Frédéric Blanqui

• PhD in progress : Jiaxiang Liu, Testing Confluence via Critical Pairs, 2012, École Polytechnique, Jean-Pierre Jouannaud

• PhD in progress: Qian Wang, CoqMTU: a secure combination of the Calculus of Construction, inductive types, universes and built-in equality, 2011, École Polytechnique, Jean-Pierre Jouannaud

Juries

• Frédéric Blanqui has been in the jury of Zhiwu Xu for his PhD on “Parametric Polymorphism for XML Processing Languages” (directors: Giuseppe Castagna and Haiming Chen).

• Frédéric Blanqui refered the habilitation thesis of René Thiemann (Innsbrück University) on “A Formalization of Termination Techniques in Isabelle/HOL”.

• Jean-François Monin has been in the jury of Xiaomu Shi (see above).

• Vania Joloboff has been in the jury of Xiaomu Shi (see above).