Past seminars
2024
Friday 12 January 2024, 13:00, room 1Z76: Trocq: Proof Transfer for Free, With or Without Univalence, Enzo Crance (Gallinette, Inria Rennes, LS2N, Mitsubishi Electric), Cyril Cohen (Inria Sophia-Antipolis)
Wednesday 10 January 2024, 10:00, room 1Z76: Fixed Point Theorems for Non-Transitive Relations, Jérémy Dubut-Kross (AIST, Tokyo)
2023
Friday 15 December 2023, 13:00, room 1Z71: Countable choice in Observational Type Theory, Loïc Pujet (University of Stockholm).
Thursday 14 December 2023, 15:00, room 1Z76: Towards a certified proof assistant kernel — What it takes and what we have, Meven Lennon-Bertrand (University of Cambridge).
Friday 1 December 2023, 15:30, room 3U47: "A quote? In *my* type theory?", Pierre-Marie Pédrot (Gallinette, Inria Rennes, LS2N).
Thursday 19 October 2023, 15:00, room 1Z76: Polarized Linear Logic with Fixpoints, Farzad Jafarrahmani (LIP6).
Thursday 21 September 2023, 14:00, room 1Z31: Applications of Homological Algebra to Algebraic Theories, Mirai Ikebuchi (Kyoto university).
Tuesday 11 July 2023, 14:00, room 3U47: Formal Reasoning using Distributed Assertions, Farah Al Wardani (LIX, Inria).
Thursday 25 May 2023, 14:00, room 1Z76: An interface for diagrammatic proofs in Coq, Luc Chabassier (LMF).
Thursday 4 May 2023, 14:00, room 1Z56: Meta-information for Proof Objects, Nicolas Méric (LMF).
Thursday 27 April 2023, 14:00, room 1Z28: Reconstruction of TLAPS proofs solved by veriT in Lambdapi, Alessio Coltellacci (Université de Lorraine, Inria Nancy).
Thursday 30 March 2023, 14:00, room 1Z34: (∞-)Categorical semantic of type theory: an introduction, El Mehdi Cherradi (IRIF).
Thursday 16 February 2023 Thursday 2 March 2023, 14:00, room 1Z56:
Retrofitting OCaml modules: An Fω-inspired approach for a modern module system,
Clément Blaudeau
(Cambium, Inria Paris).
Thursday 12 January 2023, 14:00, room 3U47: Intersection Types in Deduction Modulo Theory, Olivier Hermant (CRI, Mines Paris, PSL University), joint work with Ronan Saillard.
Wednesday 11 January 2023, 13:00, room 1Z53: From Metamath to Dedukti, and beyond!, Amélie Ledein (Deducteam).
Monday 9 January 2023, 10:00, room 3U47 and recorded (due to technical problems it starts around 8:10): Translating proofs from an impredicative type system to a predicative one, Thiago Felicissimo (Deducteam), joint work with Frédéric Blanqui and Ashish Kumar Barnawal.
2022
Thursday 8 December 2022, 14:00, room 3U42 and online: Impredicativity, comprehension scheme, polymorphism and bar recursion, Valentin Blot (Deducteam).
Thursday 17 November 2022, 17:00, room 3U42 and online: Lean in Practice as a Theorem Prover and Functional Programming Language, Rishikesh Vaishnav (San Diego University master student).
Wednesday 16 November 2022, 14:00: Machine Learning and Autoformalisation, Anthony Bordg (Cambridge University).
Thursday 6 October 2022, 2:00 PM, room 3U42: Strong normalisation in a System F modulo isomorphisms, Cristian Sottile (Universidad de Buenos Aires).
Wednesday 13 July 2022, 10:30 AM, room 3U42: Stability of mergesort, almost for free, Kazuhiko Sakaguchi (University of Tsukuba).
Thursday 7 July 2022, 2:00 PM, room 3U42: A Rewriting Logic Approach to Specification, Proof-search, and Meta-proofs in Sequent Systems, Carlos Olarte (LIPN, Université Sorbonne Paris Nord), joint work with Elaine Pimentel and Camilo Rocha.
Thursday 30 June 2022, 11:30 AM, room 3U47 and online: Composable Partial Multiparty Session Types, Claude Stolze (Université d'Udine, Italie).
Thursday 31 March 2022, 2:00 PM, room 3U47 and online: Extending SMTCoq with Abductive Reasoning, Arjun Viswanathan (University of Iowa).
Thursday 24 March 2022, 3:00 PM, room 3U47 and online: Vers une traduction de K en Dedukti, Amélie Ledein (Deducteam, INRIA, LMF, Université Paris-Saclay).
Thursday 17 February 2022, 10:30 AM, room 3U47 and online: A Framework for Proving Ontology-Relations and Testing Ontology Instances, Burkhart Wolff (LMF, Université Paris-Saclay).
2021
Thursday 4 November 2021, 10:30 AM, room 3U47: Récit d’exploration libre d’un traducteur humain dans les galaxies formelles d’univers mathématiques, Roland Coghetto.
Thursday 28 October 2021, 2:00 PM, room 3U47: Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting, Michael Färber (University of Innsbruck).
Thursday 21 October 2021, 10:00 AM, room 1X59 and online: La confluence de règles dans les calculs d'ordre supérieur avec types dépendants, Jean-Pierre Jouannaud (deducteam).
Thursday 14 October 2021, 2:00 PM, room 3U47 and online: SSProve: A foundational framework for modular cryptographic proofs in Coq, Théo Winterhalter (MPI-SP, Bochum, Germany).
Friday 10 September 2021, 11:00 AM, room 3U47: On what is wrong with higher-order SMT and what we are doing to fix it, Sophie Tourret (INRIA, LORIA).
Friday 23 July 2021, 3:00 PM, online: Inductive Aspects of Set-Theoretic Models of Sized CIC, Yufeng Li (University of Waterloo, Canada).
Thursday 25 March 2021, 15:00, online: Le Framework K, Amélie Ledein (LMF, deducteam).
Thursday 11 March 2021, 14:00, online: Geometry of Interaction for ZX-Diagrams, Kostia Chardonnet (LMF) and Renaud Vilmart (deducteam, LMF).
Thursday 4 February 2021, 14:00, online: The Taming of the Rew: A Type Theory with Computational Assumptions, Théo Winterhalter (MPI)
2020
Thursday 14 December 2020, 14:00, online: A new connective in propositional logic, Gilles Dowek (LSV, équipe deducteam), joint work (in progress) with Alejandro Díaz-Caro.
Thursday 1 October 2020, 14:00, LSV 3U47 + online: Illustrations mathématiques, l'exemple des tores plats polyhedraux, Alba Málaga (LORIA, équipe Gamble).
Thursday 17 September 2020, 15:30, LSV + online: Définitions et preuves inductives en théorie des types dépendants, Amélie Ledein (M2 intern, deducteam).
Thursday 2 July 2020, 10:00, online: Certification modulaire de Why3, Quentin Garchery (PhD student, VALS, LRI, Univ. Paris-Saclay).
Thursday 25 June 2020, 14:00, online: Implicit automata in typed λ-calculi, Tito (Lê Thành Dũng) Nguyễn (PhD student, LIPN, Univ. Paris Nord).
Thursday 18 June 2020, 14:00, online: Elpi, the extension language for your ITP, Enrico Tassi (marelle, Inria Sophia antipolis).
Thursday 11 June 2020, 14:00, online: Minimal Concurrent Proof Checking, Michael Färber (deducteam, LSV).
Thursday 27 February 2020, 14:00, LSV library: Dependent Type Theory in Polarised Sequent Calculus, Étienne Miquey (Post-doc, Deducteam).
Thursday 20 February 2020, 14:00, LSV library: Matching Logic: Theory and Proofs, Dorel Lucanu (Alexandru Ioan Cuza University), joint work with Traian Serbanuta, Xiaohong Chen and Grigore Rosu.
Thursday 6 February 2020, 14:00, LSV library: Formal study of the French tax code's implementation, Denis Mérigoux (Prosecco, inria Paris).
Thursday 30 January 2020, 14:00, LSV library: Functional Verification of Tezos Smart Contracts in Coq, Raphaël Cauderlier (nomadic labs).
Thursday 23 January 2020, 10:00, LSV library: Two talks, François Charton, Guillaume Lample (facebook).
2019
Thursday 12 December 2019, 14:00, LSV library: Capturing exact measures of evaluation with non-idempotent types in classical natural deduction, Pierre Vial (Post-doc, Galinette).
Thursday 14 November 2019, 14:00, LSV library: Dependent type theories as "cellular" Lawvere theories (joint work with P. LeFanu Lumsdaine), Chaitanya Leena Subramaniam (PhD student, IRIF).
Thursday 7 November 2019, 14:00, LSV library: Maintaining a mechanized language semantics across several proof assistants: a call for solutions, Arthur Charguéraud (iCube).
Thursday 24 October 2019, 14:00, LSV library: Checking HOL Proof Terms, Michael Färber (deducteam, LSV).
Thursday 10 October 2019, 14:00, LSV library: Type classes in Isabelle, Michael Färber (post-doc, deducteam, LSV).
Thursday 10 October 2019, 15:00, LSV library: Interoperability between CTS, François Thiré (PhD student, deducteam, LSV).
Thursday 19 September 2019, 14:00, LSV library: Importing Agda proofs in Logipedia, Guillaume Genestier (PhD student, Deducteam).
Monday 16 September 2019, 14:00, LSV library: Prophecy Variables in Separation Logic, Rodolphe Lepigre (post-doc, MPI).
Wednesday 4 September 2019, 14:00, LSV library: Subject reduction in Lambdapi and injectivity of function symbols in term rewriting, Jui-Hsuan (M1 intern, ENS Ulm).
Tuesday 27 August 2019, 11:00, LSV library: Vscode extension for lambdapi based on LSP, Houda Mouzoun (M1 intern, ENSEEIHT).
Thursday 25 July 2019, 09:30, LSV library: Efficient pattern-matching in Dedukti, Gabriel Hondet (M2 intern, ENAC).
Thursday 25 July 2019, 10:30, LSV library: Subject reduction in Lambdapi and injectivity of function symbols, Jui-Hsuan (M1 intern, ENS Ulm).
Thursday 25 July 2019, 11:30, LSV library: Induction to fibred multicategory, Farzad Jafarrahmani (Master intern, ENS Cachan).
Thursday 25 July 2019, 14:00, LSV library: Ekstrakto, a tool to reconstruct Dedukti proofs from TSTP files, Yacine El Haddad (Deducteam PhD student).
Thursday 18 July 2019, 10:30, LSV library: Modèles catégoriques de la théorie des types (2eme séance), Valentin Blot (Deducteam).
Thursday 11 July 2019, 14:00, LSV library: Orienting Axioms into Rewriting Rules - Proof of Concept , Guillaume Rousseau (L3 intern, ENS Lyon).
Thursday 27 June 2019, 14:00, LSV library: Modèles catégoriques de la théorie des types (1ere séance), Valentin Blot (Deducteam).
Thursday 20 June 2019, 14:00, LSV library: Isabelle technology for the Archive of Formal Proofs, Makarius Wenzel.
Thursday 20 June 2019, 15:00, LSV library: Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting, Guillaume Genestier (Deducteam PhD student).
Thursday 20 June 2019, 16:30, LSV library: Cumulative Types Systems and levels, François Thiré (Deducteam PhD student).
Tuesday 18 June 2019, 11:00, Pavillon du Jardin, ENS Cachan: Interaction with Formal Mathematical Documents in Isabelle/PIDE, Makarius Wenzel.
Thursday 13 June 2019, 14:00, LSV library: Scallina: on the Intersection of Scala and Gallina, Youssef El Bakouny (PhD student at CNAM Paris and École Supérieure d'Ingénieurs de Beyrouth).
Thursday 16 May 2019, 14:00, LSV library: Une structure logique unifiée pour l'axiome du choix, l'induction barrée et leurs principales conséquences. , Hugo Herbelin (IRIF).
Monday 13 May 2019, 10:30, LSV library: The size-change principle for mixed induction and coinduction, Pierre Hyvernat (LAMA).
Thursday 11 April 2019, 14:00, LSV library: Monoids up to Coherent Homotopy in Two-Level Type Theory, Hugo Moeneclaey (intern at Stockholm University).
Thursday 07 March 2019, 14:00, LSV library: Dérivées et distances sur les programmes fonctionnels probabilistes, Thomas Ehrhard (IRIF).
Thursday 31 January 2019, 14:00, LSV library: Definitional Proof-Irrelevance without K, Matthieu Sozeau (IRIF).
Monday 21 - Wednesday 23 January 2019, ENS Cachan, Laplace building: Logipedia kickoff meeting.
Tuesday 08 January 2019, 14:00, ENS Cachan, Pavillon des Jardins: Integrating Rewriting, Tableau and Superposition into SMT, PhD defense of Guillaume Bury.
2018
Thursday 13 December 2018, 14:00, LSV library: A sequent calculus with dependent types for classical arithmetic, Etienne Miquey (Gallinette).
Thursday 8 November 2018, 14:00, LSV library: The intuitionistic calculus that was discovered 6 times, Stéphane Graham-Lengrand (Parsifal).
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 post-doc).
Thursday 28 June 2018, 15:00, LSV library: Tactics and certificates in Meta Dedukti, Raphaël Cauderlier (IRIF post-doc).
Thursday 28 June 2018, 14:00, LSV library: Sharing a library between proof assistants: reaching out to the HOL family, François Thiré (Deducteam PhD student).
Thursday 21 June 2018, 14:00, LSV library: Drags: a new framework for graph rewriting and its impact on termination criteria, Jean-Pierre Jouannaud (Université Paris-Sud, Ecole Polytechnique).
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 PhD student)
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 (PhD student at 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 post-doc).
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 post-doc).
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.
