Publications

  • International Journals
    • Paul Brauner, Fabrice Nahon, Claude Kirchner and Hélène Kirchner - « Inductive proof search modulo ». In Annals of Mathematis and Artificial Intelligence, 2009.
    • Guillaume Burel and Claude Kirchner - « Regaining Cut Admissibility in Deduction Modulo using Abstract Completion ». Information and Computation, 208:140-164, 2010.
    • Olivier Hermant - « Resolution is Cut-Free ». Journal of Automated Reasoning, 44(3): 245-276, 2010.
    • Olivier Hermant, James Lipton - « Completeness and Cut-elimination in the Intuitionistic Theory of Types - Part 2 ». Journal of Logic and Computation 20(2): 597-602, 2010.
  • International conferences
    • Guillaume Burel - « Automating Theories in Intuitionistic Logic ». FroCoS (Silvio Ghilardi et Roberto Sebastiani, éd.), Lecture Notes in Artificial Intelligence, vol. 5749, Springer, 2009, p.181-197.
    • Guillaume Burel - « Embedding Deduction Modulo into a Prover ». In the 19th EACSL Annual Conference on Computer Science Logic (A. Dawar et H. Veith, éd.), Lecture Notes in Computer Science, vol. 6247, Springer, 2010, p.155-169.
    • Denis Cousineau - « Complete reducibility candidates » . In proceedings of PSTT09.
    • Cody Roux and Frederic Blanqui - « On the relation between size-based termination and semantic labelling ». In the 18th EACSL Annual Conference on Computer Science Logic, Lecture Notes in Computer Science, vol. 5771, Springer, 2009, p.147-162.
    • Clément Houtmann - « Axiom Directed Focusing ». Post-Proceedings of TYPES 2008, LNCS 5497, 2009.
    • Gilles Dowek - « Polarized Resolution Modulo , IFIP Theoretical Computer Science, 2010.
    • Gilles Dowek - « On the convergence of reduction-based and model-based methods in proof theory ». Logic Journal of the Interest Group in Pure and Applied Logic, 2009.
    • Gilles Dowek - « Skolemization in Simple Type Theory: the Logical and the Theoretical Points of View » Festschriftin Honour of Peter B. Andrews on his 70th Birthday. College Publications, 2008.
    • Chantal Keller and Benjamin Werner - « Importing HOL Light into Coq ». Proceedings of ITP'2010.
  • International workshops
    • Mathieu Boespflug. « Conversion by evaluation ». In Proceedings of the Twelfth International Symposium on Pracical Aspects of Declarative Languages, Madrid, Spain, 2010. A preliminary version was presented at the NbE'09 workshop.
    • Mathieu Boespflug. « From self-interpreters to normalization by evaluation ». In Informal Proceedings of the 2009 Workshop on Normalization by Evaluation, pages 29-34, Los Angeles, California, August 2009.
    • Guillaume Burel and Gilles Dowek « How can we prove that a proof search method is not an instance of another ». Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice. ACM International Conference, 2009.
    • Gilles Dowek - « Specifying programs with propositions and with congruences » (manuscript).
    • Gilles Dowek - « Simple Type Theory as a Clausal Theory » (manuscript).
  • PhD Thesis
    • Lisa Allali - « Coupures et réécriture. La super-cohérence comme critère universel de l'élimination des coupures. » Thèse de l'école polytechnique, 2010.
    • Guillaume Burel - « Bonnes démonstrations en déduction modulo ». Thèse de doctorat, Université Henri Poincaré (Nancy 1), 2009.
    • Paul Brauner - « Fondements et mise-en-oeuvre de la Super Déduction Modulo ». Thèse de doctorat, INPL, 2010.
    • Denis Cousineau - « Models and proof normalization ». Thèse de l'école polytechnique, 2009.
    • Clément Houtmann - « Représentation et interaction des preuves en superdéduction modulo ». Thèse de doctorat, Université Henri Poincaré (Nancy 1), 2010.