This page contains references to my papers and their presentation, the talks I gave as well as my Ph.D. thesis manuscript and other unpublished work. A separate page lists my papers by year.

Papers and Talks

Journal articles

  1. G. Dowek and O. Hermant, A Simple Proof that Super-Consistency Implies Cut Elimination, Notre-Dame Journal of Formal Logic, 53:4, pp. 439-456, 2012: [pdf], [bibtex]
  2. O. Hermant, Resolution is Cut-Free, Journal of Automated Reasoning, 44(3), pp. 245-276, 2010: [pdf], [bibtex]
  3. O. Hermant and J. Lipton, Cut elimination in the Intuitionistic Theory of Types with Axioms and Rewriting Cuts, Constructively, in: C. Benzmüller, C. E. Brown, J. Siekmann and R. Stateman, eds., Festschrift in Honor of Peter B. Andrews on his 70th Birthday, Studies in Logic and the Foundations of Mathematics, IfCoLog, 2008: [pdf], [bibtex]
  4. O. Hermant and J. Lipton, Completeness and cut elimination in the Intuitionistic Church's Theory of Types - Part 2, Journal of Logic and Computation, 20(2), pp. 597-602, March 2010: [pdf], [bibtex]
  5. O. Hermant, Skolemization in various intuitionistic logics, Archive for Mathematical Logic, 2008 (to appear): ps and pdf coming soon, [bibtex]

Proceedings of international conferences

  1. G. Gilbert and O. Hermant, Normalisation by completeness with Heyting algebras, in: M. Davis, A. Fehnker, A. McIver and A. Voronkov (eds), LPAR 20, LNCS ARCoSS 9450, pp. 469-482, 2015: [pdf], [bibtex]
  2. G. Bury, D. Delahaye, D. Doligez, P. Halmagrand and O. Hermant, Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo, in: A. Fehnker, A. McIver, G. Sutcliffe and A. Voronkov (eds),LPAR 20 (short papers), EPiC Series in Computing 35, pp. 42--58, 2015: [url] [pdf], [bibtex]
  3. L. Allali and O. Hermant, Semantic A-Translations and Super-Consistency entail Classical Cut Elimination, in: K. McMillan, A. Middeldorp and A. Voronkov (eds), LPAR 19, LNCS ARCoSS 8312, pp. 407-422, 2013: [pdf], [bibtex]
  4. M. Boudard and O. Hermant, Polarizing Double-Negation Translations, in: K. McMillan, A. Middeldorp and A. Voronkov (eds), LPAR 19, LNCS ARCoSS 8312, pp. 182-197, 2013: [pdf], [bibtex].
  5. D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand and O. Hermant, Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo, in: K. McMillan, A. Middeldorp and A. Voronkov (eds), LPAR 19, LNCS ARCoSS 8312, pp. 274-290, 2013: [pdf], [bibtex].
  6. G. Le Truong, D. Fedosov, O. Hermant, M. Manceny, R. Pawlak and R. Rioboo, Programming Robots with Events, in G. Schirner, Marcelo Götz, A. Rettberg, M. C. Zanella and F. Rammig (eds), IESS 2013, IFIP Advances in Information and Communication Technology 403, pp. 14-25, 2013.
  7. G. Le Truong, O. Hermant, M. Manceny, R. Pawlak and R. Rioboo, Using Event-Based Style for Developing M2M Applications, in J. Park, H. Arabnia, C. Kim, W. Shi and J.-M. Gil (eds), Grid and Pervasive Computing 2013, LNCS 7861, pp. 348-357, 2013.
  8. Denis Cousineau, Olivier Hermant, A Semantic Proof that Reducibility Candidates entail Cut Elimination, RTA 2012, LiPICS 15, pp. 133-148, 2012: [url], [pdf], [bibtex].
  9. G. Le Truong, O. Hermant, M. Manceny, R. Pawlak and R. Rioboo, Unifying Event-based and Rule-based Styles to Develop Concurrent and Context-aware Reactive Applications - Toward a Convenient Support for Concurrent and Reactive Programming, ICSOFT 2012, SciTePress, pp. 347-350, 2012: [pdf], [bibtex]
  10. A. Brunel, O. Hermant and C. Houtmann, Orthogonality and Boolean Algebras for Deduction Modulo, TLCA'11, LNCS 6990, pp. 76-90, Springer, 2011. [pdf], [ps], [ps.gz], [bibtex]
    Slides of the presentation: [ps], [ps.gz], [pdf]
  11. O. Hermant and J. Lipton, A constructive semantic approach to cut elimination in type theories with axiom, CSL'08, LNCS 5213, pp. 169-183, 2008: [pdf], [bibtex].
  12. G. Dowek and O. Hermant, A simple proof that super-consistency implies cut elimination, proceedings of RTA'07, LNCS 4533, pp. 93-106, 2007: [ps], [ps.gz], [pdf], [bibtex], [link]
    Slides of the presentation: [ps], [ps.gz], [pdf]
  13. R. Bonichon and O. Hermant, On constructive semantic cut admissibility in deduction modulo, post-proceedings of TYPES'06, LNCS 4502, pp. 41-50, 2007: [ps], [ps.gz], [pdf], [bibtex], [link]
  14. R. Bonichon and O. Hermant, A semantic completeness proof for TaMeD, proceedings of LPAR'06, Phnom Penh, Cambodia, LNCS 4246, pp. 167-181, 2006: [ps], [ps.gz], [pdf], [bibtex], [link]
    Slides of the presentation (by Richard Bonichon): [ps], [ps.gz], [pdf]
  15. O. Hermant, Semantic cut elimination in the Intuitionnistic Sequent Calculus, proceedings of TLCA'05, Nara, Japan, LNCS 3461, pp. 221-233, 2005: [ps], [ps.gz], [pdf], [bibtex], [link]
    Slides of the presentation: [ps], [ps.gz], [pdf]

In international workshops (with proceedings and committee)

  1. V. Maisonneuve, O. Hermant and F. Irigoin, Computing Invariants with Transformers: Experimental Scalability and Accuracy, proceedings of NSAD, ENTCS 307, pp. 17-31, 2014.
  2. D. Delahaye, D. Doligez, F. Gilbert, P. Halamagrand and O. Hermant, Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps, in IWIL, 10th International Workshop on the Implementation of Logics, 2013: [pdf] [bibtex]
  3. D. Delahaye, D. Doligez, F. Gilbert, P. Halamagrand and O. Hermant, Proof Compression and Certification in Zenon Modulo, Third Workshop of the Amadeus Project on Proof Compression, Nancy, 2013.
  4. M. Boespflug, Q. Carbonneaux and O. Hermant, The λΠ-calculus Modulo as a Universal Proof Language, PxTP 2012, 878, pp. 28-43, 2012: [pdf], [bibtex], [link]
  5. O. Hermant, K. Khramenkova and R. Pawlak, Simulator of a "Weather" Cloud, 10th Finnish-Russian University Cooperation in Telecommunication workshop (FRUCT), Tampere, Finland, 2011
  6. O. Hermant, G. Le-Truong, M. Manceny, R. Pawlak, Dynamic Adaptation through Event Reconfiguration, VADER Workshop, 2011, Hersonissos, Crete, Greece. In R. Meersman, T. Dillon and P. Herrero (eds), On the Move to Meaningful Internet Systems: OTM 2011 Workshops, LNCS 7046, pp. 637-646
  7. O. Hermant, A Model-based cut elimination proof, 2nd St-Petersburg Days of Logic and Computability, St-Pétersbourg, 2003: [ps], [ps.gz], [pdf], [bibtex]
    Slides of the presentation: [ps], [ps.gz], [pdf]


  1. E. J. Gallego Arias, O. Hermant and P. Jouvelot, Verification of Faust Signal Processing Programs in Coq, CoqPL Workshop, Mumbai, January 2015: [pdf]
  2. UFRN, Natal (Brasil) LoLITA & ForAll Workshop, 1 Dec. 2014, invited speaker, Double Negation Translations as Morphisms: [pdf]
  3. O. Hermant, Encoding Zenon Modulo in Dedukti, 2nd KWARC-Deducteam Workshop, Bremen, 12 May 2014: [pdf]
  4. V. Maisonneuve, O. Hermant and F. Irigoin, ALICe: A Framework to Improve Affine Loop Invariant Computation, 5th workshop on Invariant Generation (WING), Vienna, July 2014: [pdf]
  5. M. Boespflug, Q. Carbonneaux, O. Hermant and R. Saillard, Dedukti: A Universal Proof Checker, Journées LLL (GDR LAC, LTP and LAMHA), Orléans, October 2012: [pdf]
  6. A linear logic modulo, 1st Workshop on Type theory, proof theory and rewriting, Paris (France), June 2007: [ps], [ps.gz], [pdf]
  7. A semantical cut elimination in intuitionistic deduction modulo, TYPES'04, Jouy-en-Josas (France), Dec. 2004: [ps], [ps.gz], [pdf]
  8. Compilation of rewrite rules, 2nd workshop on Coq + rewriting, Ecole polytechnique, Palaiseau (France), 2004: [ps], [ps.gz], [pdf]

Talks and seminars

  • Deducteam, Paris (France), 12 Dec. 2014, Double Negation Translations as Morphisms: [pdf]
  • CRI, Fontainebleau (France), 2 Jun. 2014, Double Dose of Double-Negation Translations: [pdf]
  • Deducteam, Paris (France), 11 May 2012, Light Polarized Translations in Deduction Modulo: [pdf]
  • PPS, Paris (France), 8 Mar. 2012, From Normalization to Cut Elimination: [pdf]
  • TODO: CORIAS, etc.
  • PPS, Paris (France), 18 Mar. 2008: [ps], [ps.gz], [pdf]
  • LIP, ENS Lyon (France), 11 Mar. 2008: [ps], [ps.gz], [pdf]
  • Wesleyan University, Middletown, CT (Etats-Unis), Dec. 2007: [ps], [ps.gz], [pdf]
  • Politecnica de Madrid (Espagne), Nov. 2007: [ps], [ps.gz], [pdf]
  • Complutense de Madrid (Espagne), Sep. 2007: [ps], [ps.gz], [pdf] and the [video]
  • Séminaire MeASI, CEA-CNRS-Ecole polytechnique (France), Jun. 2007: [ps], [ps.gz], [pdf]
  • Wesleyan University, Middletown, CT (Etats-Unis), Dec. 2006: [ps], [ps.gz], [pdf]
  • Créteil (France), invited, Oct. 2007: [ps], [ps.gz], [pdf]
  • Keio University, Tokyo (Japon), Jun.-Jui. 2006: talk on the blackboard, a A1 poster: [pdf]
  • Univ. Paris 11, LRI, Orsay (France), May 2006: [ps], [ps.gz], [pdf]
  • Univ. Paris 7, PPS, Paris (France), Jan. 2004: [ps], [ps.gz], [pdf]
  • Marktoberdorf (Allemagne), Aug. 2003: [ps], [ps.gz], [pdf]

Ph.D. Thesis

The abstract of my Ph.D. thesis and of the defense.
The Ph.D. thesis manuscript: [ps], [ps.gz], [pdf], [pdf.gz], [bibtex]
Here are the slides of the defense: [ps], [ps.gz], [pdf]



Here, some draft documents, that have not (yet) been turned into papers:
  • A linear logic modulo: [ps], [ps.gz], [pdf]
  • Compilation of rewriting rules towards an abstract machine: [ps], [ps.gz], [pdf]
  • Completness of Cut-Free Sequent Calculus Modulo (2004, 28 pp.):[ps], [ps.gz], [pdf]. Extension of the Saint Petersburg paper with a lot more conditions on rewrite rules.
  • Italian Master thesis (2002), named: "Déduction modulo et élimination des coupures: une approche syntaxique". I here study the link between resolution (modulo) and the cut free sequent calculus. In french with an italian foreword: [ps], [ps.gz], [pdf]