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 mailinglist for announcements, go
there.
2015
 20150710, 10:00, Vert 1 room, Term Inference and Unification in Lambda Pi Calculus Modulo,
Gaëtan Gilbert.
Details here.
 20150703, 10:00, Orange 2 room, Every superpolynomial proof in purely implicational minimal logic
has a polynomially sized proof in classical implicational propositional logic,
Hermann Haeusler.
Details here.
 20150626, 10:00, Orange 2 room, Lambdacalculus, Sharing, and Time Cost Models,
Beniamino Accattoli.
Details here.
 20150612, 10:00, Rose room, From linear logic to process algebras:
focusing and partialorder reduction,
David Baelde.
Details here.
 20150605, 10:00, Orange 2, The explog normal form of types and canonical forms of terms,
Danko Ilik.
Details here.
 20150529, 10:00, Orange 2 room, Synthesis for Communicationcentred Programming,
Mariangiola Dezani &
Works in progress in type theory modulo type isomorphisms,
Alejandro DíazCaro.
Details here.
 20150522, 10:30, Vert 2 room, Automated verification of security protocols: the case of indistinguishablity,
Steve Kremer.
Details here.
 20150417, 10:00, Orange 2 room, The cost of usage in the lambdacalculus,
JeanJacques Lévy.
Details here.
 20150403, 10:00, Rose room, Protocol security: a proof theoretic perspective,
Hubert Comon.
Details here.
 20150327, 10:00, Orange 2 room, Formal verification of numerical computations:
application to the 1D wave equation,
Sylvie Boldo.
Details here.
 20150325, 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.
 20150320, 10:00, Rose room, Analysing privacytype properties in cryptographic protocols,
Stéphanie Delaune.
Details here.
 20150313, 10:00, Orange 2 room, Semantics for Higher Order Constraint Logic Programming,
Jim Lipton.
Details here.
 20150306, 10:00, Rose room, Confluence of layered systems,
JeanPierre Jouannaud.
Details here.
 20150220, 10:00, Vert 1 room, Teaching Zenon how to count,
Guillaume Bury.
Details here.
 20150213, 10:00, Orange 2 room, A Constructive Proof of the Topological Kruskal Theorem,
Jean GoubaultLarrecq.
Details here.
 20150206, 10:30, Orange 2 room, Intuitionnistic checker for classical proofs, The Imitation Game,
Zakaria Chihani.
Details here.
 20150130, 10:30, Orange 2 room, Defining the semantics of proof evidence,
Dale Miller.
Details here.
 20150123, 10:00, Orange 2 room,
Wedding Boolean Solvers with Superposition: a Societal Reform,
Simon Cruanes.
Details here.
2014
 20141216, 10:00, Vert 2 room, Past, Present and Future of Nuprl,
Vincent Rahli.
Details here.
 20141212, 10:00, Orange 2 room, Double Negation Translations as Morphisms,
Olivier Hermant.
Details here.
 20141128, 10:00, Orange 2 room, New advances on mimpgraph representation,
Vaston Costa.
Details here.
 20141121, 10:00, Orange 2 room, Zelus, a synchronous language with Ordinary Differential Equations,
Marc Pouzet.
Details here.
 20141114, 10:00, Vert 1 room, Implementing an interactive proof system,
Arnaud Spiwack.
Details here.
 20141107, 10:30, Orange 2 room, A Superposition Calculus for Abductive Reasoning,
Nicolas Peltier.
Details here.
 20141031, 10:00, Vert 1 room, dTL2: Differential Temporal Dynamic Logic with Nested
Modalities for Hybrid Systems,
JeanBaptiste Jeannin.
Details here.
 20141024, 10:00, Vert 1 room, Cut admissibility by saturation,
Guillaume Burel.
Details here.
 20141017, 10:00, Orange 2 room, Relation Algebra, Allegories, and Logic Programming,
Emilio Jesús Gallego Arias.
Details here.
 20141010, 10:00, Orange 2 room, A point on fixpoints in posets,
Frédéric Blanqui.
Details here.
 20141003, 10:00, Orange 2 room,
Models and termination of proofreduction in the lambdaPicalculus modulo theory,
Gilles Dowek.
Details here.
 20140926, 10:00, Vert 1 room, Mechanising large formal proofs: an example,
JeanRaymond Abrial.
Details here.
 20140919, 10:00, Orange 2 room, Dependent Typing for Multirate Faust,
Pierre Jouvelot.
Details here.
 20140912, 10:00, Orange 2 room, SMT and Traces,
Pascal Fontaine (Veridis, LORIA).
Details here.
 20140905, 11:00, Orange 2 room, Theorem Proving using Deep Inference,
Kaustuv Chaudhuri.
Details here.
 20140711, 10:00, Bleu 1 room, Sharing resources in a proof by means of reference instead of copying,
Vaston Costa.
Details here.
 20140627, 10:00, Orange 2 room, Logtk : A Logic ToolKit for Automated Reasoning and its Implementation,
Simon Cruanes.
Details here.
 20140613, 10:00, Orange 2 room, Quantitative Types for HigherOrder Languages,
Delia Kesner.
Details here.
 20140523, 10:00, Orange 2 room, AltErgo: An SMT Solver For Program Verification,
Mohamed Iguernelala.
Details here.
 20140516, 11:00, Orange 2 room, Agda's Secret  On the Design and Implementation of the Agda Language,
Andreas Abel.
Details here.
 20140516, 09:30, Orange 2 room, ChurchRosser Properties of Positional Abstract Rewriting Systems,
JeanPierre Jouannaud.
Details here.
 20140425, 10:00, Vert 1 room, Towards an Internalization of the Groupoid Model of Type Theory,
Matthieu Sozeau.
Details here.
 20140425, 10:00, Vert 1 room, About equality in type theory,
Hugo Herbelin (π.r^{2}, Inria & Université Paris Diderot).
Details here.
 20140411, 14:00, Rose room, The FoCaLiZe language: mixing program and proofs,
François Pessaux.
Details here.
 20140404, 10:00, Orange 2 room,
The Implicit Calculus of Constructions with Σtypes (ICC_{Σ}),
Bruno Bernardo (Ecole polytechnique).
Details here.
 20140328, 10:00, Orange 2 room, Reflecting Inductive Types in Type Theory,
PierreEvariste Dagand (Gallium, Inria).
Details here.
 20140314, 10:00, Vert 2 room, Some Methods of proof compression,
Vaston Costa (Universidade Federal de Goiás).
Details here.
 20140307, 10:00, Vert 1 room, Natural Algorithms,
Bernadette CharronBost (LIX, Ecole polytechnique).
Details here.
 20140221, 10:00, Vert 1 room, Objects and Subtyping in the λΠcalculus modulo,
Raphaël Cauderlier (CPR, CNAM & Deducteam, Inria).
Details here.
 20140207, 10:00, Orange 2 room, special session on type isomorphisms:
 Simply typed lambdacalculus modulo type isomorphisms,
Alejandro DíazCaro (U. Paris Ouest & Deducteam).
 Isomorphisms in presence of sum and function types,
Danko Ilik (Parsifal, Inria & LIX).
Details here.
2013
 20131213, 10:00, Vert 2 room, A short discussion on nonstandard finite computation,
Edward Hermann Haeusler (PUC Rio).
Details here.
 20131122, 10:00, Orange 2 room, A prooftheoretical discussion on the mechanization of
propositional logics, Edward Hermann Haeusler (PUC Rio).
Details here.
 20131115, 10:00, Orange 2 room Redesigning the LCFstyle architecture for tableauxlike/Prologlike
proofsearch and SMTsolving, Stéphane GrahamLengrand, (CNRS & Ecole polytechnique).
Details here.
 20131018, 14:00, Vert 2 room, Yet Another Complete Rewrite of Dedukti,
Ronan Saillard, (CRI, MINES ParisTech & Deducteam, INRIA).
Details here.
 20131018, 10:00, Vert 1 room, An introduction to Homotopy Type Theory,
Bruno Barras, (Marelle, LIX, CNRS & INRIA Saclay & Ecole polytechnique).
Details here.
 20130913, 10:00, Orange 1 room, Detection of First Order Axiomatic Theories,
Simon Cruanes (Deducteam, INRIA & Ecole polytechnique).
Details here.
 20130711, 10:00, Orange 2 room, Generate and check method for invariant verification in CafeOBJ,
Kokichi Futatsugi (JAISTRCSV). Details here.
 20130705, 10:00, Bleu 1 room The Computability Path Ordering,
JeanPierre Jouannaud. Details here.
 20130503, 10:00, Vert 1 room, A Quantum Programming Language,
Benoît Valiron (University of Pennsylvania).
Details here.
 20130412, Orange 1 & Orange 2 rooms, KWARCDeducteam workshop
Details here.
 20130329, 10:00, Bleu 1 room, LALBLC: a program testing the equivalence of dpda's,
Géraud Sénizergues (LABRI, Université de Bordeaux).
Details here.
 20130322, 10:00, Rose room, Extending Propositional Dynamic Logic to Petri Nets,
Bruno Lopes. Details here.
 20130315, 10:00, Vert 2 room, Applications and metamathematical implications of
Doublenegation Shift, Danko Ilik (independent researcher).
Details here
 20130215, 10:00, Vert 2 room, Mining malware specifications through static reachability
analysis, Hugo Macedo (Deducteam, INRIA). Details here.
 20130201, 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.
 20130125, 10:00, Orange 2 room, The Univalence Axiom,
Ronan Saillard (CRI, Mines ParisTech and Deducteam, INRIA).
Details here.
2012
 20121130, 10:00, Vert 1 room, Embedding constructiveness into
classical logic via double negation translations or polarization,
Florence Clerc (Parsifal, INRIASaclay).
Details here.
 20121123, 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.
 20121116, 10:00, Vert 2 room, Defining coinductive types in secondorder subtractive logic
(and getting a coroutinebased implementation of streams), Tristan Crolar (CPR, CEDRIC, CNAM).
Details here.
 20121109, 10:00, Orange 1 room, Constructivism: from nonrigorous philosophy to
rigorous mathematics, Jaime Gaspar (PiR2, INRIA ParisRocquencourt).
Details here.
 20121019, 10:00, Orange 2 room, Arbitrary multitruthvalue functions and Natural Deduction,
Cecilia Englander (PUC Rio). Details here.
 20121012, 16:00, Orange 1 room, Non determinism through type isomophism,
Alejandro DíazCaro, (Université de Paris Ouest and Deducteam, INRIA).
Details here.
 20121005, 14:00, Orange 1 room, Reasoning modulo Equality and Equations,
Simon Cruanes (Deducteam, INRIA and CPR, CEDRIC, ENSIIECNAM).
Details here.
 20120928, 10:00, Vert 2 room,ML Dependency Analysis for Assessors,
Vincent Benayoun (CPR, CEDRIC, CNAM). Details here.
 20120907, 10:00, Orange 1 room,Termination by Jumping and Escaping,
Nachum Dershowitz(TelAviv University). Details here.
 20120803, 10:00, Vert 2 room, Proof Theory for some diagrammatic logical proofs,
Mitsuhiro Okada (Keio University). Details here.
 20120720, 10:00, Rose room, Canonical Inference, Nachum Dershowitz
(Tel Aviv University). Details here.
 20120706, 10:00, Vert 1 room, A Certified Constraint Solver over Finite Domains,
Catherine Dubois (CPR, Cedric, CNAM & ENSIIE and Deducteam, INRIA). Details
here.
 20120629, 14:00, Jaune room, From physics to interrupt handlers: the real to float step,
Vivien Maisonneuve (CRI, Mines ParisTech). Details here.
 20120608, 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.
 20120511, 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.
 20120406, 10:00, Rose room, First order reasoning in Yices 2, Simon Cruanes
(SRI, EPFL and Ecole polytechnique). Details here.
2011
 20111216, 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.

20111202, 17:30, Vert 1 room, A constructive approach to classical modal logic,
Luiz Carlos Pereira (PUCRio). Details here.
 20111125, 10:00, CNAM, 33119, AltErgo : AC(X) et traces "légères" en Coq,
Sylvain Conchon (LRI, Proval). Details here.
 20110704, 10:00, INRIA
 An introduction to Atelier B, David Delahaye (CPR, CEDRIC, CNAM) and
Mélanie Jacquel (CPR, CEDRIC, CNAM and Siemens).
 Realizability and SuperConsistency, Tomás Lungenstrass
(Ecole polytechnique).
Details here.
 20110622, 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.
 20110527, INRIA
 Dedukti, Mathieu Boespflug (Mc Gill University).
 Traduction de HOL en Dedukti, Chantal Keller (Ecole polytechnique).
Details here.
 20110510, 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.
 20110401, 9:00, INRIA
 Currystyle vs Churchstyle in deduction modulo, Denis Cousineau (Microsoft Research).
 Generalizing Boolean Algebras for deduction modulo, Olivier Hermant (LISITE, ISEP).
 Firstorder 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.