Section: Dissemination

Promoting Scientific Activities

Scientific Events Organisation

Member of the Organizing Committees

Yann Régis-Gianas is multimedia chair of the organizing committee of POPL 2017 that will be held in Paris in January 2017.

Yves Guiraud, Philippe Malbos and Samuel Mimram have organised the second edition of the Higher-Dimensional Rewriting and Applications (HDRA) workshop of the Formal Structures for Computation and Deduction conference (FSCD), held in Porto in June 2016. They plan to organise the third edition of HDRA, still with FSCD, in September 2017 in Oxford.

Yves Guiraud and Alexis Saurin, with Christine Tasson (IRIF), have organised the annual meeting of the Géocal and LAC working groups of the GDR Informatique Mathématique in Paris, in November 2016.

Yves Guiraud and Samuel Mimram, with Dimitri Ara (Univ. Aix-Marseille) are currently organising the Categories in Homotopy and Rewriting one-week conference, that will be held at the CIRM, in Marseille, in September 2017.

Scientific Events Selection

Member of the Conference Program Committees

Matthieu Sozeau was member of the program committees of FSCD'16, ITP'16 and CoqPL'16.

Member of the Conference Steering Committees

Hugo Herbelin is a member of the steering committee of the conference Formal Structures for Computation and Deduction (FSCD).

Pierre-Louis Curien is member of the steering committee of the international workshop Games for Logic and Programming Languages (GaLop).

Matthieu Sozeau is member of the steering committee of the Dependently Typed Programming international workshop (DTP).

Journal

Member of the Editorial Boards

Pierre-Louis Curien is editor in chief of the Cambridge University Press journal Mathematical Structures in Computer Science (since January 2016).

Reviewer - Reviewing Activities

The members of the team reviewed papers for numerous journals and international conferences.

Invited Talks

Pierre-Louis Curien and Samuel Mimram gave invited talks at the annual meeting of the Géocal and LAC working groups of the GDR Informatique Mathématique (Paris, November).

Pierre-Louis Curien gave an invited talk at the annual meeting of the international ANR project Pace (between Univ. of Bologna, ENS Lyon and Shanghai Jiaotong University) on “Categorified cyclic operads” (Shanghai, November).

Hugo Herbelin gave an invited talk on “Proving with side-effects” at the Days in Logic meeting in Lisbon, Portugal.

Jean-Jacques Lévy gave an invited talk about “Strongly connected components in graphs, Formal proof of Tarjan 1972 algorithm” at the LTP (Langages, Types et Preuves) day, Saclay [38].

Matthieu Sozeau gave invited talks at the DeepSpec kickoff meeting in Princeton, NJ, USA, June 8th 2016, on “Coq 8.6” (together with Maxime Dénès), at the International Conference on Mathematical Software in Berlin, Germany, July 14th 2016, on “Coq for HoTT”, at the Categorical Logic and Univalent Foundations workshop, Leeds, UK, July 28th 2016, on “Forcing Translations in Type Theory”, and at the Coq Workshop in Nancy, France, August 26th 2016, on “Coq 8.6”.

Scientific Expertise

Pierre-Louis Curien has been member of the “Comité de Sélection” for a professor position in discrete mathematics at the University Paul Sabatier in Toulouse.

Yann Régis-Gianas and Hugo Herbelin have been members of the “Comité de Sélection” for an assistant professor position at CNAM in Paris.

Yann Régis-Gianas has been member of the “Comité de Sélection” for an assistant professor position at IRIF in Paris.

Hugo Herbelin has been member of the “Comité de Sélection” for a starting researcher position at Inria Saclay.

Scientific expertise

Pierre-Louis Curien is a member of the Scientific Committee of the CIRM (since June 2013).

Research Administration

Pierre-Louis Curien, Hugo Herbelin and Yves Guiraud are members of the scientific council of the Computer Science deparment of University Paris 7.

Yves Guiraud is the head of the Preuves, Programmes and Systèmes (PPS) team of the IRIF laboratory (since April 2016), and a member of the IRIF council (since January 2016).

Presentation of papers

Étienne Miquey gave a talk on a computational reduction of dependent choice in classical logic to system F at TYPES'16 (Novi Sad, Serbia, May 2016).

Étienne Miquey gave a talk on realizability games for the specification problem during the workshop Realizability in Uruguay 2016 (Piriápolis, Uruguay, July 2016).

Cyrille Chenavier gave a talk at the workshop IWC, Obergurgl, Austria (September 2016).

Cyrille Chenavier, Maxime Lucas and Jovana Obradović gave talks at the workshop Categories, Homotopy and Rewriting (Toulouse, January) and at the workshop HDRA (Porto, June).

Jovana Obradović presented her works on cyclic operads at the Types Conference 2016 (Novi Sad, Serbia, May 2016) and at the Conference Logic and Applications 2016 (Dubrovnik, Croatia, September).

Hugo Herbelin gave a talk on proving Gödel's completeness theorem with side-effects at the Mathematics for Computation workshop in Niederalteich, Germany, May 2016.

Talks in seminars

Pierre-Louis Curien gave a talk at the Séminaire de Topologie of the University of Angers on the semantics of dependent types (January).

Yves Guiraud gave a talk in the Séminaire de Combinatoire of the University Paris 7 on an introduction to Squier's theory (November).

Hugo Herbelin gave a talk on a proof-as-program interpretation of the classical axiom of dependent choice at the Séminaire “Logique et Interactions” of the “Logique de la Programmation” team of the “Institut de Mathématiques de Marseille” (University Aix-Marseille, February).

Yann Régis-Gianas gave a talk about control operators in the history of programming at the Séminaire “Code Sources” organized by Baptiste Mélès.

Yann Régis-Gianas gave a talk about the writing style in programming at the conference “Current issues in the philosophy of practice of mathematics and informatics” (University of Toulouse, April).

Thibaut Girka gave a talk about difference languages at the Gallium seminar (Paris, September 2016) and at the TLP group of the GDR GPL (Saclay, November 2016).

Yann Régis-Gianas gave a talk about difference languages at the LIMA laboratory (Nantes, October 2016) and at the Semantic Working Group of IRIF (Paris, December 2016).

Matthieu Sozeau gave a talk about Equations: a function definition toolbox for Coq at Dagstuhl in March 2016.

Cyrille Chenavier gave a talk about confluence algebras at the Algebra working group of the LMPA, Calais, in February 2016.

Jovana Obradović gave a talk about categorified cyclic operads at the Proof Theory Seminar of the Mathematical Institute of the Serbian Academy of Sciences and Arts (Belgrade, December 2016).

Attendance to conferences, workshops, schools,...

Pierre-Louis Curien attended the conferences Types 2016 in Novi Sad (Serbia, May) and Logic and Applications in Dubrovnik (Croatia, September).

Cyrille Chenavier, Pierre-Louis Curien, Yves Guiraud, Maxime Lucas, Philippe Malbos, Samuel Mimram and Jovana Obradović attended the Category, Homotopy and Rewriting workshop in Toulouse (January 2016).

Cyrille Chenavier, Maxime Lucas, Philippe Malbos and Samuel Mimram attended the HDRA workshop in Lisbon (June 2016).

Hugo Herbelin attended the Days in Logic meeting in Lisbon (Portugal, January), the Mathematics for Computation workshop in Niederalteich (Germany, May), the conferences Types 2016 in Novi Sad (Serbia, May), the Coq coding sprint in Sophia-Antipolis (May-June), the DeepSpec kick-off meeting in Princeton (USA, June), the FSCD conference in Porto (Portugal, June), the Coq workshop and ITP 2016 (Nancy, August), as well as the Dagstuhl seminar on universality of proofs (October).

Jean-Jacques Lévy participated to CPP and POPL 2016 conferences, Saint Petersburgh, USA, January 18-22, and the Robin Milner Award reception, the Royal Society, London, November 24 (X. Leroy (research team Gallium) was awarded).

Matthieu Sozeau attended POPL 2016, ICMS 2016, ITP 2016, the Coq coding sprint, the DeepSpec kick-off meeting in Princeton as well as the Dagstuhl seminar on proofs of functional programs (March).

Théo Zimmermann attended the conference CICM 2016 in Białystok (Poland, July). He gave a talk there to present his PhD subject. He also attended the Coq coding sprint.

Groupe de travail Théorie des types et réalisabilité

This is one of the working groups of PPS, jointly organised by Hugo Herbelin and Matthieu Sozeau.

Groupe de travail Catégories supérieures, polygraphes et homotopie

Several members of the team participate actively in this weekly working group of PPS, organised by François Métayer (IRIF) since 2009.