# Past seminars

## 2018

**Thursday 27 September 2018**, 14:00, LSV library: Rewrite tactic in Lambdapi, Aristomenis-Dionysios Papadopoulos (Intern Imperial College, London).

**Thursday 20 September 2018**, 14:00, LSV library: Termination checking using well-founded typing derivations, Rodolphe Lepigre (Deducteam).

**Thursday 28 June 2018**, 15:00, LSV library:
Tactics and certificates in Meta
Dedukti, Raphaël
Cauderlier (IRIF).

**Thursday 28 June 2018**, 14:00, LSV library:
Sharing a library between proof
assistants: reaching out to the HOL
family, François
Thiré (Deducteam).

**Thursday 21 June 2018**, 14:00, LSV library:
Drags: a new framework for graph rewriting and its impact on
termination criteria, Jean-Pierre Jouannaud.

**Tuesday 10 April 2018**, 9:00, Room F580, Halle
aux Farines, Université Denis Diderot,
Paris: Extending higher-order logic
with predicate subtyping (PhD defense), Frédéric Gilbert
(Deducteam)

**Thursday 5 April 2018**, 14:00, LSV:
Translating between lambda calculi
with different qubit representation, Agustín Borgna
(Universidad de Buenos Aires).

**Monday 19 March 2018**, 14:00, Amphi Chemla, ENS Cachan: Upscale meeting

**Thursday 1 March 2018**, 14:00, LSV
library: An introduction to
certified programming using Agda, Mathieu Montin (IRIT).

**Thursday 15 February 2018**, 13:30, LSV library:
Intersection Types in Deduction
Modulo
Theory, Olivier
Hermant (MINES Paris Tech).

**Thursday 25 January 2018**, 16:30, ENS Cachan,
Pavillon des Jardins: Practical
Curry-Style using Choice Operators, Local Subtyping and Circular
proofs, Rodolphe Lepigre
(Deducteam).

## 2017

**Tuesday 12 December 2017**, 11:00, ENS Cachan, Pavillon des Jardins: Building proof automations in dependently-typed languages to make Type-Driven Development come true, Franck Slama (University of St Andrews, UK).

**Tuesday 16 November 2017**, 14:00, LSV: An introduction to Bindlib in the context of Dedukti, Rodolphe Lepigre (Deducteam).

**Tuesday 7 November 2017**, 11:00, ENS Cachan, Pavillon des Jardins: Realizability: denotational semantics for correctness, Valentin Blot (LRI).

**Thursday 5 October 2017**, 13:30, ENS Cachan, Pavillon des Jardins: Environments and the Complexity of Abstract Machines, Bruno Barras (Inria).

**Tuesday 26 September 2017**, 11:00, ENS Cachan, Pavillon des Jardins: Linking Focusing and Resolution with Selection, Guillaume Burel (ENSIIE).

**Tuesday 19 September 2017**, 11:00, ENS Cachan, Pavillon des Jardins: Semantics and Implementation of an Extension of ML for Proving Programs, Rodolphe Lepigre (Inria).

**Thursday 14 September 2017**, 10:30, LSV: Foundations of Dependent Interoperability, Pierre-Evariste Dagand (CNRS, LIP6).

**Thursday 20 July 2017**, 10:00, LSV: A complete and terminating strategy for the Bana-Comon equivalence logic, Adrien Koutsos (LSV).

**Friday 7 July 2017**, LSV, 10:00: Deduction modulo in Zipperposition: past, present, and future, Simon Cruanes (INRIA Nancy).

**Tuesday 20 June 2017**, ENS Cachan, Pavillon des Jardins, 11:00: Quantum Digital Physics, Pablo Arrighi (LIF, Université Aix-Marseille).

**Tuesday 13 June 2017**, ENS Cachan, Amphi Chemla, 11:00: A Curry-Howard Approach to Tree Automata, Colin Riba (LIP, Ens Lyon).

**Tuesday 30 May 2017**, 14:00: Models of type theory given by program translation, Simon Boulier (EPI Ascola, Nantes).

**Thursday 4 May 2017**, 14:00: A Transfer Tactic for Dedukti and its Application to Interoperability, Raphaël Cauderlier (IRIF).

**Tuesday 2 May 2017**, ENS Cachan, Pavillon des Jardins, 11:00: Binary-level security analysis: semantics to the rescue!, Sébastien Bardin and Richard Bonichon (CEA).

**Thursday 27 April 2017**, 14:00: Automatic and Transparent Transfer of Theorems along (Iso)morphisms in the Coq Proof Assistant, Théo Zimmermann (πr²).

**Thursday 20 April 2017**, 14:00, Room L106, Mines ParisTech, 60 bd St Michel, Paris: Habilitation, Olivier Hermant (Mines ParisTech).

**Thursday 6 April 2017**, 14:00: A lambda calculus for density matrices, Alejandro Díaz-Caro (CONICET, Universidad Nacional de Quilmes).

**Thursday 30 March 2017**, 14:00: An interpretation of system F through bar recursion, Valentin Blot (Queen Mary University of London).

**Tuesday 28 March 2017**, 11:00: ENS Cachan, Bât. Institut D'Alembert, Auditorium Daniel Chemla, A formal set-theoretical model of Coq and its application to strong normalization, Bruno Barras (INRIA Saclay, LIX).

**Thursday 23 March 2017**, 14:00: Extending Higher-order Logic with Predicate Subtyping, Frédéric Gilbert (Deducteam).

**Thursday 2 March 2017**, 9:00: Tactics and certificates in Meta Dedukti, Raphaël Cauderlier (IRIF).

## 2016

**Friday 16 December 2016**, 10:30: Out-of-order processing of Coq documents, Enrico Tassi (INRIA Sophia-Antipolis).

**Friday 16 December 2016**, 9:00: Computer-Aided Verification of Mechanism Design: Challenges in the Combination of Interactive Proof Systems, Emilio Jesús Gallego Arias (MINES ParisTech).

**Saturday 10 December 2016**, 14:00, CNAM, 292 rue Saint-Martin, Paris, amphithéâtre Abbé-Grégoire: Déduction Automatique et Certification de Preuve pour la Méthode B, PhD defense, Pierre Halmagrand (CNAM).

**Wednesday 7 December 2016**, 16:30: Categorical Semantics of Logic Programming Languages (part 6), Jim Lipton (Wesleyan University).

**Friday 2 December 2016**, 10:30: EasyCrypt, yet another theorem prover, Pierre-Yves Strub (LIX).

**Wednesday 30 November 2016**, 16:30: Categorical Semantics of Logic Programming Languages (part 5), Jim Lipton (Wesleyan University).

**Wednesday 23 November 2016**, 16:30: Categorical Semantics of Logic Programming Languages (part 4), Jim Lipton (Wesleyan University).

**Wednesday 16 November 2016**, 16:30, LSV: Categorical semantics of logic programming languages (part 3), Jim Lipton (Wesleyan University).

**Tuesday 15 November 2016**, 14:00: Isabelle/PIDE - from Interactive Theorem Proving to Integrated Theorem Proving, Makarius Wenzel (Technische Universität München, Germany).

**Friday 4 November 2016**, 10:30: Towards Hybrid Theorem Proving Interfaces, Emilio Jesús Gallego Arias (Mines ParisTech).

**Wednesday 2 November 2016**, 16:30, LSV: Categorical semantics of logic programming languages (part 2), Jim Lipton (Wesleyan University).

**Friday 28 October 2016**, 14:00, LRI, building 650, room 445, rue Noetzlin, Gif-sur-Yvette: Encoding of polymorphic universes in LPMod, Jean-Pierre Jouannaud (Université Paris-Sud and Ecole Polytechnique).

**Friday 28 October 2016**, 10:00, LRI, building 660, amphitheater: Seminar LRI-LSV on Verification and Proofs, Chantal Keller (LRI) and Gilles Dowek (LSV).

**Thursday 27 October 2016**, 16:30, LSV: Categorical semantics of logic programming languages (part 1), Jim Lipton (Wesleyan University).

**Thursday 27 October 2016**, 14:00, LSV: Reconstruction de preuves au format TSTP pour Dedukti (short talk), David Pham (ENSIIE intern).

**Sunday 16 - Friday 21 October 2016**: Dagstuhl seminar on the universality of proofs.

**Friday 14 October 2016**, 10:30: Reverse engineering en arithmetics proofs: from Matita to Hol, François Thiré (Deducteam).

**Monday 10 October 2016**, 10:00, room 21.2.3, CNAM, 292 rue Saint-Martin, Paris, PhD defense: Mécanismes Orientés-Objet pour l'Interopérabilité entre Systèmes de Preuves, Raphaël Cauderlier.

**Monday 10 October 2016**, 10:30, INRIA Saclay, room Gilles Kahn: Confluence of rewrite systems based on decreasing diagrams, PhD defense, Jiaxiang Liu (Ecole Polytechnique).

**Friday 30 September 2016**, 14:00: MMT: A UniFormal Approach to Knowledge Representation, Florian Rabe (Jacobs University, Bremen, Germany).

**Friday 23 September 2016**, 10:30: A Unified Procedure for Provability and Counter-Model Generation in Minimal Implicational Logic, Jefferson Santos (Pontifícia Universidade Católica do Rio de Janeiro, Brazil).

**Friday 27 May 2016**, 10:30: Tests and Proofs for Enumerative Combinatorics , Catherine Dubois (ENSIIE).

**Friday 20 May 2016**, 10:30: Formalizing Computation, Nachum Dershowitz (Tel Aviv University and Institut d'Etudes Avancées de Paris).

**Friday 13 May 2016**, 10:30: Decidability, Introduction Rules and Automata, Gilles Dowek (Inria).

**Friday 22 April 2016**, 10:30: Automated constructivisation of proofs, Frédéric Gilbert (Inria/CEA/NASA).

**Friday 8 April 2016**, 10:30: Size-based termination for higher-order rewriting (2nd part), Frédéric Blanqui (Inria).

**Friday 1st April 2016**, 10:30: GPO: a total well-founded monotonic path ordering for directed rooted labelled graphs, Jean-Pierre Jouannaud (Université Paris-Saclay, École Polytechnique).

**Friday 25 March 2016**, 10:30: Size-based termination for higher-order rewriting (1st part), Frédéric Blanqui (Inria).

**Friday 18 March 2016**, 10:30: Linking Focusing and Resolution with Selection, Guillaume Burel (ENSIIE).

**Friday 11 March 2016**, 10:30: Archsat: SMT, Tableaux and beyond, Guillaume Bury (Inria).

**Friday 26 February 2016**, 10:30: Proof Constructivization in Meta-Dedukti, Raphaël Cauderlier (Cnam/Inria).

**Friday 12 February 2016**, 10:30: Contextual types for multi-staged programming, Matthias Puech (Université Paris Diderot).

**Tuesday 9 February 2016**, 11:00: Quis custodiet ipsos custodes? - Trusting theorem provers, Giselle Reis (Inria).

**Friday 5 February 2016**, 10:30: Automated Deduction and Proof Certification for the B Method Set Theory, Pierre Halmagrand (Cnam/Inria).

**Friday 22 January 2016**, 10:30: Matching concepts across formalized libraries, Thibault Gauthier (University of Innsbruck).

## 2015

**Friday 11 December 2015**,
10:30: Call-by-value, call-by-name and
Geometry of Interaction, Benoît
Valiron (Centrale Supélec).

**Friday 4 December 2015**,
10:30: An axiom free Coq proof of
Kruskal's tree
theorem, Dominique
Larchey (CNRS, LORIA, Nancy).

**Friday 20 November 2015**,
10:30: Reversible Causal Graph
Dynamics, Simon Martiel.

**Tuesday 6 October 2015**, 10:00-19:00, ENS Cachan: Journée PML-Dedukti.

**Monday 28 September 2015**, 15:00, INRIA Paris, 23 avenue d'Italie, room Orange: A framework for defining computational higher-order logics, PhD defense of Ali Assaf.

**Friday 25 September 2015**, 10:00, University Paris-Diderot, Sophie Germain building, room 1006: Model Checking and Theorem Proving, PhD defense of Kailiang Ji.

**Friday 25 September 2015**, 15:00, MINES ParisTech, 60 Boulevard Saint-Michel, 75006 Paris, room V115: Typechecking in the λΠ-Calculus Modulo: Theory and Practice, PhD defense of Ronan Saillard.

**Friday 18 September 2015**, 10:00, INRIA Paris, 23 avenue Italie, room Orange: Un Calcul des Constructions implicite avec sommes dépendantes et à inférence de type décidable, PhD defense of Bruno Bernardo.

**Thursday 10 September 2015**, 15:00, École Polytechnique, amphi Cauchy: Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond, PhD defense of Simon Cruanes.