The Deducteam Seminar

This page is no longer maintained since August 2015. Please see the new page there

There was a Google agenda for the seminars available here. Ical version here. The detailed page of the seminar containing all the abstracts is here. To subscribe or unsuscribe to the mailing-list for announcements, go there.

2015

• 2015-07-10, 10:00, Vert 1 room, Term Inference and Unification in Lambda Pi Calculus Modulo, Gaëtan Gilbert. Details here.
• 2015-07-03, 10:00, Orange 2 room, Every super-polynomial proof in purely implicational minimal logic has a polynomially sized proof in classical implicational propositional logic, Hermann Haeusler. Details here.
• 2015-06-26, 10:00, Orange 2 room, Lambda-calculus, Sharing, and Time Cost Models, Beniamino Accattoli. Details here.
• 2015-06-12, 10:00, Rose room, From linear logic to process algebras: focusing and partial-order reduction, David Baelde. Details here.
• 2015-06-05, 10:00, Orange 2, The exp-log normal form of types and canonical forms of terms, Danko Ilik. Details here.
• 2015-05-29, 10:00, Orange 2 room, Synthesis for Communication-centred Programming, Mariangiola Dezani &
  Works in progress in type theory modulo type isomorphisms, Alejandro Díaz-Caro. Details here.
• 2015-05-22, 10:30, Vert 2 room, Automated verification of security protocols: the case of indistinguishablity, Steve Kremer. Details here.
• 2015-04-17, 10:00, Orange 2 room, The cost of usage in the lambda-calculus, Jean-Jacques Lévy. Details here.
• 2015-04-03, 10:00, Rose room, Protocol security: a proof theoretic perspective, Hubert Comon. Details here.
• 2015-03-27, 10:00, Orange 2 room, Formal verification of numerical computations: application to the 1D wave equation, Sylvie Boldo. Details here.
• 2015-03-25, 10:00, Orange 2 room, special session on encodings in Dedukti,
  • Focalizing on Dedukti, Raphaël Cauderlier.
  • The Chicken and the Pencil, Ali Assaf.
  Details here.
• 2015-03-20, 10:00, Rose room, Analysing privacy-type properties in cryptographic protocols, Stéphanie Delaune. Details here.
• 2015-03-13, 10:00, Orange 2 room, Semantics for Higher Order Constraint Logic Programming, Jim Lipton. Details here.
• 2015-03-06, 10:00, Rose room, Confluence of layered systems, Jean-Pierre Jouannaud. Details here.
• 2015-02-20, 10:00, Vert 1 room, Teaching Zenon how to count, Guillaume Bury. Details here.
• 2015-02-13, 10:00, Orange 2 room, A Constructive Proof of the Topological Kruskal Theorem, Jean Goubault-Larrecq. Details here.
• 2015-02-06, 10:30, Orange 2 room, Intuitionnistic checker for classical proofs, The Imitation Game, Zakaria Chihani. Details here.
• 2015-01-30, 10:30, Orange 2 room, Defining the semantics of proof evidence, Dale Miller. Details here.
• 2015-01-23, 10:00, Orange 2 room, Wedding Boolean Solvers with Superposition: a Societal Reform, Simon Cruanes. Details here.

2014

• 2014-12-16, 10:00, Vert 2 room, Past, Present and Future of Nuprl, Vincent Rahli. Details here.
• 2014-12-12, 10:00, Orange 2 room, Double Negation Translations as Morphisms, Olivier Hermant. Details here.
• 2014-11-28, 10:00, Orange 2 room, New advances on mimp-graph representation, Vaston Costa. Details here.
• 2014-11-21, 10:00, Orange 2 room, Zelus, a synchronous language with Ordinary Differential Equations, Marc Pouzet. Details here.
• 2014-11-14, 10:00, Vert 1 room, Implementing an interactive proof system, Arnaud Spiwack. Details here.
• 2014-11-07, 10:30, Orange 2 room, A Superposition Calculus for Abductive Reasoning, Nicolas Peltier. Details here.
• 2014-10-31, 10:00, Vert 1 room, dTL2: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems, Jean-Baptiste Jeannin. Details here.
• 2014-10-24, 10:00, Vert 1 room, Cut admissibility by saturation, Guillaume Burel. Details here.
• 2014-10-17, 10:00, Orange 2 room, Relation Algebra, Allegories, and Logic Programming, Emilio Jesús Gallego Arias. Details here.
• 2014-10-10, 10:00, Orange 2 room, A point on fixpoints in posets, Frédéric Blanqui. Details here.
• 2014-10-03, 10:00, Orange 2 room, Models and termination of proof-reduction in the lambda-Pi-calculus modulo theory, Gilles Dowek. Details here.
• 2014-09-26, 10:00, Vert 1 room, Mechanising large formal proofs: an example, Jean-Raymond Abrial. Details here.
• 2014-09-19, 10:00, Orange 2 room, Dependent Typing for Multirate Faust, Pierre Jouvelot. Details here.
• 2014-09-12, 10:00, Orange 2 room, SMT and Traces, Pascal Fontaine (Veridis, LORIA). Details here.
• 2014-09-05, 11:00, Orange 2 room, Theorem Proving using Deep Inference, Kaustuv Chaudhuri. Details here.
• 2014-07-11, 10:00, Bleu 1 room, Sharing resources in a proof by means of reference instead of copying, Vaston Costa. Details here.
• 2014-06-27, 10:00, Orange 2 room, Logtk : A Logic ToolKit for Automated Reasoning and its Implementation, Simon Cruanes. Details here.
• 2014-06-13, 10:00, Orange 2 room, Quantitative Types for Higher-Order Languages, Delia Kesner. Details here.
• 2014-05-23, 10:00, Orange 2 room, Alt-Ergo: An SMT Solver For Program Verification, Mohamed Iguernelala. Details here.
• 2014-05-16, 11:00, Orange 2 room, Agda's Secret -- On the Design and Implementation of the Agda Language, Andreas Abel. Details here.
• 2014-05-16, 09:30, Orange 2 room, Church-Rosser Properties of Positional Abstract Rewriting Systems, Jean-Pierre Jouannaud. Details here.
• 2014-04-25, 10:00, Vert 1 room, Towards an Internalization of the Groupoid Model of Type Theory, Matthieu Sozeau. Details here.
• 2014-04-25, 10:00, Vert 1 room, About equality in type theory, Hugo Herbelin (π.r², Inria & Université Paris Diderot). Details here.
• 2014-04-11, 14:00, Rose room, The FoCaLiZe language: mixing program and proofs, François Pessaux. Details here.
• 2014-04-04, 10:00, Orange 2 room, The Implicit Calculus of Constructions with Σ-types (ICC_Σ), Bruno Bernardo (Ecole polytechnique). Details here.
• 2014-03-28, 10:00, Orange 2 room, Reflecting Inductive Types in Type Theory, Pierre-Evariste Dagand (Gallium, Inria). Details here.
• 2014-03-14, 10:00, Vert 2 room, Some Methods of proof compression, Vaston Costa (Universidade Federal de Goiás). Details here.
• 2014-03-07, 10:00, Vert 1 room, Natural Algorithms, Bernadette Charron-Bost (LIX, Ecole polytechnique). Details here.
• 2014-02-21, 10:00, Vert 1 room, Objects and Subtyping in the λΠ-calculus modulo, Raphaël Cauderlier (CPR, CNAM & Deducteam, Inria). Details here.
• 2014-02-07, 10:00, Orange 2 room, special session on type isomorphisms:
  • Simply typed lambda-calculus modulo type isomorphisms, Alejandro Díaz-Caro (U. Paris Ouest & Deducteam).
  • Isomorphisms in presence of sum and function types, Danko Ilik (Parsifal, Inria & LIX).
  Details here.

2013

• 2013-12-13, 10:00, Vert 2 room, A short discussion on non-standard finite computation, Edward Hermann Haeusler (PUC Rio). Details here.
• 2013-11-22, 10:00, Orange 2 room, A proof-theoretical discussion on the mechanization of propositional logics, Edward Hermann Haeusler (PUC Rio). Details here.
• 2013-11-15, 10:00, Orange 2 room Re-designing the LCF-style architecture for tableaux-like/Prolog-like proof-search and SMT-solving, Stéphane Graham-Lengrand, (CNRS & Ecole polytechnique). Details here.
• 2013-10-18, 14:00, Vert 2 room, Yet Another Complete Rewrite of Dedukti, Ronan Saillard, (CRI, MINES ParisTech & Deducteam, INRIA). Details here.
• 2013-10-18, 10:00, Vert 1 room, An introduction to Homotopy Type Theory, Bruno Barras, (Marelle, LIX, CNRS & INRIA Saclay & Ecole polytechnique). Details here.
• 2013-09-13, 10:00, Orange 1 room, Detection of First Order Axiomatic Theories, Simon Cruanes (Deducteam, INRIA & Ecole polytechnique). Details here.
• 2013-07-11, 10:00, Orange 2 room, Generate and check method for invariant verification in CafeOBJ, Kokichi Futatsugi (JAIST-RCSV). Details here.
• 2013-07-05, 10:00, Bleu 1 room The Computability Path Ordering, Jean-Pierre Jouannaud. Details here.
• 2013-05-03, 10:00, Vert 1 room, A Quantum Programming Language, Benoît Valiron (University of Pennsylvania). Details here.
• 2013-04-12, Orange 1 & Orange 2 rooms, KWARC-Deducteam workshop Details here.
• 2013-03-29, 10:00, Bleu 1 room, LALBLC: a program testing the equivalence of dpda's, Géraud Sénizergues (LABRI, Université de Bordeaux). Details here.
• 2013-03-22, 10:00, Rose room, Extending Propositional Dynamic Logic to Petri Nets, Bruno Lopes. Details here.
• 2013-03-15, 10:00, Vert 2 room, Applications and meta-mathematical implications of Double-negation Shift, Danko Ilik (independent researcher). Details here
• 2013-02-15, 10:00, Vert 2 room, Mining malware specifications through static reachability analysis, Hugo Macedo (Deducteam, INRIA). Details here.
• 2013-02-01, 10:00, Orange 2 room, Session on automatic theorem proving:
  • Automated recognition of axiomatic theories in an automated prover, Simon Cruanes (Ecole polytechnique and Deducteam, INRIA)
  • Proofs and finite models, Cailiang Yu (Deducteam, INRIA).
  Details here.
• 2013-01-25, 10:00, Orange 2 room, The Univalence Axiom, Ronan Saillard (CRI, Mines ParisTech and Deducteam, INRIA). Details here.

2012

• 2012-11-30, 10:00, Vert 1 room, Embedding constructiveness into classical logic via double negation translations or polarization, Florence Clerc (Parsifal, INRIA-Saclay). Details here.
• 2012-11-23, 10:00, Algorithme room, On Graph Calculi for Relations, Paulo A. S. Veloso (Federal University of Rio de Janeiro, COPPE: Systems and Computer Engineering Programme). Details here.
• 2012-11-16, 10:00, Vert 2 room, Defining co-inductive types in second-order subtractive logic (and getting a coroutine-based implementation of streams), Tristan Crolar (CPR, CEDRIC, CNAM). Details here.
• 2012-11-09, 10:00, Orange 1 room, Constructivism: from non-rigorous philosophy to rigorous mathematics, Jaime Gaspar (PiR2, INRIA Paris-Rocquencourt). Details here.
• 2012-10-19, 10:00, Orange 2 room, Arbitrary multi-truth-value functions and Natural Deduction, Cecilia Englander (PUC Rio). Details here.
• 2012-10-12, 16:00, Orange 1 room, Non determinism through type isomophism, Alejandro Díaz-Caro, (Université de Paris Ouest and Deducteam, INRIA). Details here.
• 2012-10-05, 14:00, Orange 1 room, Reasoning modulo Equality and Equations, Simon Cruanes (Deducteam, INRIA and CPR, CEDRIC, ENSIIE-CNAM). Details here.
• 2012-09-28, 10:00, Vert 2 room,ML Dependency Analysis for Assessors, Vincent Benayoun (CPR, CEDRIC, CNAM). Details here.
• 2012-09-07, 10:00, Orange 1 room,Termination by Jumping and Escaping, Nachum Dershowitz(Tel-Aviv University). Details here.
• 2012-08-03, 10:00, Vert 2 room, Proof Theory for some diagrammatic logical proofs, Mitsuhiro Okada (Keio University). Details here.
• 2012-07-20, 10:00, Rose room, Canonical Inference, Nachum Dershowitz (Tel Aviv University). Details here.
• 2012-07-06, 10:00, Vert 1 room, A Certified Constraint Solver over Finite Domains, Catherine Dubois (CPR, Cedric, CNAM & ENSIIE and Deducteam, INRIA). Details here.
• 2012-06-29, 14:00, Jaune room, From physics to interrupt handlers: the real to float step, Vivien Maisonneuve (CRI, Mines ParisTech). Details here.
• 2012-06-08, Vert 1 and Rose rooms, Day on computation in quantic physics and logic, talks by:
  • Pablo Arrighi (IMAG),
  • Maël Pégny,
  • Pierre Néron (Ecole polytechnique and INRIA),
  • Raphaël Bost (Ecole polytechnique and INRIA),
  • Ali Assaf (Ecole polytechnique and INRIA),
  • Quentin Carbonneaux (Ponts ParisTech and INRIA),
  • Raphaël Cauderlier (ENS Cachan and INRIA),
  • Guillaume Burel, (CPR, Cédric, ENSIIE),
  • David Delahaye (CPR, Cédric, CNAM),
  • Mélanie Jacquel (Siemens and CPR, Cédric, CNAM).
  Details here.
• 2012-05-11, 14:00, Bleu 2 room
  • Translations between Intuitionistic and Classical Logic, Mélanie Boudard (ISEP).
  • Polarized Translation for Polarized Deduction Modulo, Olivier Hermant (LISITE, ISEP).
  Details here.
• 2012-04-06, 10:00, Rose room, First order reasoning in Yices 2, Simon Cruanes (SRI, EPFL and Ecole polytechnique). Details here.

2011

• 2011-12-16, 14:30, Equation room
  • Rewriting and fixed point definitions, David Baelde (ITU Copenhaguen).
  • Eliminating Division and Square Root in Embedded Programs, Pierre Néron (INRIA and Ecole Polytechnique).
  Details here.
• 2011-12-02, 17:30, Vert 1 room, A constructive approach to classical modal logic, Luiz Carlos Pereira (PUC-Rio). Details here.
• 2011-11-25, 10:00, CNAM, 33-1-19, Alt-Ergo : AC(X) et traces "légères" en Coq, Sylvain Conchon (LRI, Proval). Details here.
• 2011-07-04, 10:00, INRIA
  • An introduction to Atelier B, David Delahaye (CPR, CEDRIC, CNAM) and Mélanie Jacquel (CPR, CEDRIC, CNAM and Siemens).
  • Realizability and Super-Consistency, Tomás Lungenstrass (Ecole polytechnique).
  Details here.
• 2011-06-22, 10:00, INRIA
  • Validation des régles de l'Atelier B, Mélanie Jacquel (CPR, CEDRIC, CNAM and Siemens).
  • On completeness of reducibility candidates as a semantics of strong normalization, Denis Cousineau (Microsoft Research).
  • Presentation of HETS, the "Heterogeneous Tool Set", Olivier Hermant (LISITE, ISEP).
  Details here.
• 2011-05-27, INRIA
  • Dedukti, Mathieu Boespflug (Mc Gill University).
  • Traduction de HOL en Dedukti, Chantal Keller (Ecole polytechnique).
  Details here.
• 2011-05-10, 13:30, Rose room
  • Clausal presentation of theories in deduction modulo, Jianhua Gao (INRIA).
  • Experimenting with deduction modulo, Guillaume Burel (CEDRIC).
  • Fitch's paradox in the light of structural proof theory, Alberto Naibo (Paris 1 University).
  Details here.
• 2011-04-01, 9:00, INRIA
  • Curry-style vs Church-style in deduction modulo, Denis Cousineau (Microsoft Research).
  • Generalizing Boolean Algebras for deduction modulo, Olivier Hermant (LISITE, ISEP).
  • First-order logic in Dedukti, Gilles Dowek (INRIA).
  • Coqine, un traducteur de preuve Coq en Dedukti, Guillaume Burel (CPR, CEDRIC, CNAM and ENSIIE).
  • Sémantique de Focalize, David Delahaye/Catherine Dubois (CPR, CNAM, CEDRIC and ENSIIE).
  Details here.

Home, Members, Software, Seminars