@PhdThesis{OHerPhD05, author = {Olivier Hermant}, title = {M\'{e}thodes S\'{e}mantiques en D\'{e}duction Modulo}, school = {Universit\'{e} Paris 7 - Denis Diderot}, year = {2005} }

@inProceedings{OHer05, author = {Olivier Hermant}, title = {Semantic cut elimination in the Intuitionistic Sequent Calculus}, year = {2005}, booktitle = {Typed Lambda-Calculi and Applications}, address = {Nara, Japan}, editor = {Pawel Urzyczyn}, series = {Lecture Notes in Computer Science} volume = {3461}, publisher = {Springer-Verlag}, pages = {221-233} }

@Article{OHer03, author = {Olivier Hermant}, title = {A Model-based Cut Elimination Proof}, year = {2003}, journal = {2nd St-Petersburg Days of Logic and Computability}, address = {Saint-Petersburg, Russia} }

@inProceedings{RBonOHer06a, author = {Richard Bonichon and Olivier Hermant}, title = {A semantic completeness proof for TaMeD}, year = {2006}, booktitle = {LPAR}, address = {Phnom Penh, Cambodia}, series = {LNCS}, volume = {4246}, publisher={Springer-Verlag}, pages={167-181} }

@InProceedings{RBonOHer06b, author = {Richard Bonichon and Olivier Hermant}, title = {On Constructive Cut Admissibility in Deduction Modulo}, pages = {33-47}, crossref = {Proc/types06} } @proceedings{Proc/types06, editor = {Thorsten Altenkirch and Conor McBride}, title = {International Workshop TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers}, booktitle = {TYPES for proofs and programs}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {4502}, year = {2007}, isbn = {978-3-540-74463-4}, issn = {0302-9743 (Print) 1611-3349 (Online)} }

@inproceedings{GDowOHer07, author = {Gilles Dowek and Olivier Hermant}, title = {A Simple Proof That Super-Consistency Implies Cut Elimination}, booktitle = {RTA}, year = {2007}, pages = {93-106}, ee = {http://dx.doi.org/10.1007/978-3-540-73449-9_9}, crossref = {DBLP:conf/rta/2007} } @proceedings{DBLP:conf/rta/2007, editor = {Franz Baader}, title = {Term Rewriting and Applications, 18th International Conference, RTA 2007, Paris, France, June 26-28, 2007, Proceedings}, booktitle = {RTA}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {4533}, year = {2007}, isbn = {978-3-540-73447-5} }

@Article{OHer08a, author = {Hermant, Olivier}, title = {Skolemization in various intuitionistic logics}, year={2008}, note={To appear}, publisher={Springer}, journal={Archive for Mathematical Logic} }

@InCollection{OHerJLip08a, author = {Olivier Hermant and James Lipton}, booktitle = {Festschrift in Honor of Peter B. Andrews on His 70th Birthday}, title = {Cut Elimination in the Intuitionistic Theory of Types with Axioms and Rewriting Cuts, Constructively}, publisher = {IFCoLog}, year = 2008, series = {Studies in Logic and the Foundations of Mathematics}, EDITOR = {Benzm{u}ller, C. E. and Brown, C. E. and Siekmann, J. and Statman, R.} }

@article{DBLP:OHerJLip10, author = {Olivier Hermant and James Lipton}, title = {Completeness and Cut-elimination in the Intuitionistic Theory of Types - Part 2}, journal = {J. Log. Comput.}, volume = {20}, number = {2}, year = {2010}, pages = {597-602}, ee = {http://dx.doi.org/10.1093/logcom/exp076}, bibsource = {DBLP, http://dblp.uni-trier.de} }

@inproceedings{OHerJLip08c, author = {Olivier Hermant and James Lipton}, title = {A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms}, booktitle = {CSL}, year = {2008}, pages = {169-183}, ee = {http://dx.doi.org/10.1007/978-3-540-87531-4_14}, crossref = {DBLP:conf/csl/2008}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/csl/2008, editor = {Michael Kaminski and Simone Martini}, title = {Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Bertinoro, Italy, September 16-19, 2008. Proceedings}, booktitle = {CSL}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {5213}, year = {2008}, isbn = {978-3-540-87530-7}, bibsource = {DBLP, http://dblp.uni-trier.de} }

@Article{OHer10, author = "Hermant, Olivier", title = "Resolution is Cut-Free", journal = "Journal of Automated Reasoning", volume = "44", number = "3", month = "March", year = "2010", pages = "245-276" }

@inproceedings{ABruOHerCHou11, author = "Alo\"{i}s Brunel, Olivier Hermant and Cl\'ement Houtmann", title = "Orthogonality and Boolean Algebras for Deduction Modulo", booktitle = {TLCA}, year = "2011", pages = {76-90} crossref = {TLCA11} } @proceedings{TLCA11, editor = {Luke Ong}, title = {Typed Lambda-Calculus and Applications Conference. Proceedings.}, booktitle = {TLCA}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6990}, year = {2011} }

@Article{GDowOHer12, author = "Dowek, Gilles and Hermant, Olivier", title = "A Simple Proof that Super-Consistency implies Cut-Elimination", journal = "Notre-Dame Journal of Formal Logic", year = "2012", volume = "53", numer = "4", pages = "439-456" }

@inProceedings{MBoeQCarOHer12, author = {Mathieu Boespflug and Quentin Carbonneaux and Olivier Hermant}, title = {The {$\lambda\Pi$}-calculus Modulo as a Universal Proof Language}, booltitle = {In Second Workshop on Proof Exchange for Theorem Proving (PxTP)}, publisher = {CEUR-WS.org}, volume = {878}, pages = {28-43}, url = {ceur-ws.org/Vol-878/paper2.pdf}, year = {2012} }

@inproceedings{DCouOHer12, author = {Denis Cousineau and Olivier Hermant}, title = {A Semantic Proof that Reducibility Candidates entail Cut Elimination}, booktitle = {RTA}, year = {2012}, pages = {133-148}, editor = {Ashish Tiwari}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, series = {LIPIcs}, volume = {15} }

@inproceedings{GLTrOHerMManRPawRRio12, author = {Truong Giang Le and Olivier Hermant and Matthieu Manceny and Renaud Pawlak and Renaud Rioboo}, title = {Unifying Event-based and Rule-based Styles to Develop Concurrent and Context-aware Reactive Applications - Toward a Convenient Support for Concurrent and Reactive Programming}, booktitle = {ICSOFT}, year = {2012}, pages = {347-350}, crossref = {icsoft2012} } @proceedings{icsoft2012, editor = {Slimane Hammoudi and Marten van Sinderen and Jos{\'e} Cordeiro}, title = {ICSOFT 2012 - Proceedings of the 7th International Conference on Software Paradigm Trends, Rome, Italy, 24 - 27 July, 2012}, booktitle = {ICSOFT}, publisher = {SciTePress}, year = {2012}, isbn = {978-989-8565-19-8} }

@inproceedings{LAllOHer13, author = {Lisa Allali and Olivier Hermant}, title = {Semantic A-Translations and Super-Consistency entail Classical Cut Elimination}, booktitle = {LPAR}, year = {2013}, pages = {407-422}, editor = {Ken McMillan and Aart Middeldorp and Andre{\"i} Voronkov}, publisher = {Springer}, series = {LNCS ARCoSS}, volume = {8312} }

@inproceedings{MBouOHer13, author = {M{\'e}lanie Boudard and Olivier Hermant}, title = {Polarizing Double-Negation Translations}, booktitle = {LPAR}, year = {2013}, pages = {182-197}, editor = {Ken McMillan and Aart Middeldorp and Andre{\"i} Voronkov}, publisher = {Springer}, series = {LNCS ARCoSS}, volume = {8312} }

@inproceedings{DDelDDolFGilPHalOHer13, author = {David Delahaye and Damien Doligez and Fr{\'e}d{\'e}ric Gilbert and Pierre Halmagrand and Olivier Hermant}, title = {Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo}, booktitle = {LPAR}, year = {2013}, pages = {274-290}, editor = {Ken McMillan and Aart Middledorp and Andre{\"i} Voronkov}, publisher = {Springer}, series = {LNCS ARCoSS}, volume = {8312} }

@inproceedings{DDelDDolFGilPHalOHer13b, author = {David Delahaye and Damien Doligez and Fr{\'e}d{\'e}ric Gilbert and Pierre Halmagrand and Olivier Hermant}, title = {Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps}, booktitle = {IWIL, 10th International Workshop on the Implementation of Logics}, year = {2013}, pages = {}, editor = {} }

@inproceedings{GBurDDelDDolPHalOHer15, author = {Guillaume Bury and David Delahaye and Damien Doligez and Pierre Halmagrand and Olivier Hermant}, title = {Automated Deduction in the {B} Set Theory using Typed Proof Search and Deduction Modulo}, booktitle = {20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations, {LPAR} 2015, Suva, Fiji, November 24--28, 2015.}, pages = {42--58}, year = {2015}, editor = {Ansgar Fehnker and Annabelle McIver and Geoff Sutcliffe and Andrei Voronkov}, series = {EPiC Series in Computing}, volume = {35}, publisher = {EasyChair}, url = {http://www.easychair.org/publications/volume/LPAR-20}, }

@inproceedings{GGilOHer15, author = {Ga{\"{e}}tan Gilbert and Olivier Hermant}, title = {Normalisation by Completeness with Heyting Algebras}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, {LPAR-20} 2015, Suva, Fiji, November 24-28, 2015, Proceedings}, pages = {469--482}, year = {2015}, editor = {Martin Davis and Ansgar Fehnker and Annabelle McIver and Andrei Voronkov}, series = {Lecture Notes in Computer Science}, volume = {9450}, publisher = {Springer}, url = {http://dx.doi.org/10.1007/978-3-662-48899-7}, doi = {10.1007/978-3-662-48899-7}, isbn = {978-3-662-48898-0}, }