2021

• Vive la Recheche en Informatique!, LMF, Univ. Paris-Saclay, 15 octobre (PDF)
• 2 talks on Finite developments in the lambda-calculus at ISR21 (12th International School on Rewriting), Madrid, 5-16 July 2021 (PDF1, PDF2, PDF3)

2019

• The four eras of Computer science, Huashang College, Guangzhou, 18 november (KEY, PDF)
• Comparing a Formal Proof in Why3, Coq, Isabelle, Nanjing University, Nanjing, 26 June;
  Institute of Software of the Chinese Academy of Sciences, Beijing, 3 July;
  LaMHA/LTP, GDR GPL, Université Paris Est, Créteil, 18 October;
  ECNU, Shanghai, 14 November; Jinan University, Guangzhou, 18 November (KEY, PDF)

2018

• Comparing a Formal Proof in Why3, Coq, Isabelle, VIP Workshop, IRIF, Univ. Paris 7, November (PDF)
• L'informatique en 4 temps, exposé Inria-Alumni à Unithé, Inria, Bordeaux, October (PDF, KEY)
• Proofs of graph algorithms with automation and their readability, Séminaire Vérification, IRIF, Univ. Paris 7, January (PDF)

2017

• Can we make readable formal proofs?, Beijing Iscas, Shanghai ECNU, Suzhou USTC, Tianjin Nankai, December (PDF, Key)
• Strongly Connected Components in graphs, formal proof of Tarjan1972 algorithm, Inria Sophia-Antipolis, Mars (PDF)
• Semi-automatic proof of Strong connectivity, journées PPS, Octobre (PDF)
• Strongly Connected Components in graphs, formal proof of Tarjan1972 algorithm, Inria Sophia-Antipolis, Mars (PDF)

2016

• Strongly Connected Components in graphs, formal proof of Tarjan1972 algorithm, Journées LTP, Plateau de Saclay, November (PDF, KEY)
• Informatique, Ecole élémentaire le Coteau, Vaucresson, Juin (PDF)

2015

• Readable proofs of DFS in graphs using Why3, Séminaire VALS, Plateau de Saclay, December (PDF, PDF4)
• The cost of usage in the lambda-calculus, Deducteam seminar, April, Chocola/ENS-Lyon, Novembre (PDF, PDF-4)
• Informatique, Ecole élémentaire le Coteau, Vaucresson, Novembre (PDF)

2014

• Simple proofs for simple programs, Journées LAC 2014, Chambéry, November (PDF, PDF4)
• Simple proofs for simple programs, (Matthew Hennessy's Fest), Lucca, October (PDF, PDF4)
• Simple proofs for simple programs, (Luca Cardelli's Fest), Cambridge, September (PDF, PDF4)
• Starts in Why3, Xidian University, Xi'an, Shaanxi, June (PDF, PDF4)
• Intuitive termination proofs, seminar SKLCS, Institute of Software, Chinese Academy of Sciences, Beijing, April (PDF, PDF4)

2013

• Experiments in Why3, Locali Workshop, Fragrant Hill, Beijing, November (PDF, PDF4), Workshop SAVE, Shanghai U., December (PDF, PDF4)
• Small bug, Big bang, seminar SKLCS, Institute of Software, Chinese Academy of Sciences, Beijing, October (PDF)
• The cost of usage in the lambda-calculus (Pierre-Louis Curien's Fest), Venice, September (PDF, PDF4, PPT, KEY)
• Understanding strong normalisation (Antonino Salibra's Fest), PPS, Paris, July (PDF, PDF4)

2012

• Joint Centre 2006-2012 (celebration of arrival of new Director Laurent Massoulié), Saclay, September, (PDF, PDF4, PPT)
• Sequentiality in Kahn-Macqueen networks and lambda-calculus (Macqueen Fest), Chicago, May, (PDF, PDF4)
• Strong Normalisation and Redex Creation in higher-order typed lambda-calculus, CEA list, April, (PDF, PDF4)

2011

• Evaluation seminar - Moscova, Paris, 23 March 2011 (PDF)
• GGJJ (revised by JJ), GGJJ event, Gérardmer, February (PDF, PPT, KEY)

2010

• Proofs, Security and Computational Sciences, The Joint Centres meeting, 5th anniversary of Cosbi, Trento, December (PDF, PPT)
• The MSR-INRIA Joint Centre, Microsoft Research Asia, Beijing, September (PDF, PPT)
• 2 talks on the λ-calculus at the 2nd Asian-Pacific Summer School on Formal Methods, Tsinghua University, August (HTML)
• Preuves de programmes et méthodes formelles, Microsoft TechDays, February (PDF, PPT)
• Un petit bogue, un grand boum, Ecole Normale Supérieure, January (HTML, PDF, Vidéo)

2009

• Lambda Calcul et Programmation, Collège de France, Seminar in Gérard Berry's Course, Paris, December (PDF, KEY, Vidéo)
• The MSR-INRIA Joint Centre, Microsoft Research Asia, Beijing; Institute of Software, Academy of Sciences, Beijing, December, (PDF)
• The MSR-INRIA Joint Centre, MSR Joint Centers meeting, Space Research Institute of Russian Academy of Sciences (IKI), Moscow, June, (PDF)
• "Combien d'Objets dans cette image?", Exposé aux professeurs de mathématiques, Académie de Versailles, Rocquencourt, June (PDF)
• The point on the MSR-INRIA Joint Centre, Visit of Rick Rashid, Orsay, June, (PDF)
• La coopération INRIA-MSR, Forum 2009, Ecole Polytechnique, Palaiseau, January, (PDF)

2008

• The MSR-INRIA Joint Centre, Barcelona Supercomputing Center (BST), University of Catalogna, Barcelona, December(PDF)
• The MSR-INRIA Joint Centre, Pôle El Chazala des Technologies de la Communication, Tunis, November (PDF)
• "Un petit bogue, un grand boum", Exposé aux professeurs de mathématiques, Académie de Versailles, Rocquencourt, October (PDF)
• "Un petit bogue, un grand boum", Unithé, INRIA, Saclay, September (PDF)
• The MSR-INRIA Joint Centre, Technical Advisory Board (TAB) meeting, Microsoft Research Cambridge, UK, June (PDF)
• The Moscova Research team, AERES, Rocquencourt, May (PDF)
• Calculabilité et Informatique, exposé aux élèves de terminale du lycée Jules Verne, Cergy-Pontoise, April (PDF)

2007

• Sharing in the Weak Lambda-Calculus, 60th Birthday of Henk Barendregt, Neijmegen, December (PDF)
• History based flow analysis in the lambda-calcululs, Nancy, November, (PDF)
• L'informatique en 4 temps, Médiatèque, Drancy, October (PDF)
• Le centre commun INRIA-MSR, ENSEEIHT, October (PDF)
• The Joint Centre, Visit of Craig Mundie, Saclay, September, (PDF)
• Small families, 60th Birthday of Gérard Huet, Ecole Normale Supérieure, July (PDF)
• Moscova 07, Comité des Projets, INRIA, Rocquencourt, Avril (PDF)
• Le Centre Commun de Recherche INRIA-Microsoft Research, ENST, April (PDF)
• The Microsoft Research-INRIA Joint Centre, opening day, Supélec, January, (PDF)

2006

• Les dominos de Wang (informatique théorique), Remise des prix du Kangourou, Université de Versailles St-Quentin, April (PDF)
• History based flow analysis in the lambda calculus, Symposium in honor of Robin Milner Ecole Polytechnique, November (PDF)
• History based flow analysis in the lambda calculus, IISc, Bangalore, February (PDF)

2005

• Sharing in the weak lambda-calculus, 60th Birthday of Jan-Willem Klop, CWI, Amsterdam, December (PDF)
• Implementation of Distribution in Process algebras, Discovery workshop, satellite of CONCUR, San Francisco, August (PDF)