Guillaume Burel, Guillaume Bury, Raphaël Cauderlier, David Delahaye, Pierre Halmagrand, et al.. First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice. Journal of Automated Reasoning, Springer Verlag, 2020, 64 (6), pp.1001-1050. ⟨10.1007/s10817-019-09533-z⟩. ⟨hal-02305831⟩

Gilles Dowek, Olivier Hermant. A simple proof that super consistency implies cut elimination. Notre Dame Journal of Formal Logic, University of Notre Dame, 2012, 53 (4), pp. 93-106. ⟨10.1215/00294527-1722692⟩. ⟨hal-00793008⟩

Olivier Hermant. Resolution is Cut-Free. Journal of Automated Reasoning, Springer Verlag, 2010, 44 (3), pp.245-276. ⟨10.1007/s10817-009-9153-6⟩. ⟨hal-00743218⟩

Olivier Hermant, James Lipton. Completeness and cut elimination in the Intuitionistic Church's Theory of Types-Part 2. Journal of Logic and Computation, Oxford University Press (OUP), 2010, Vol. 20 (No 2), pp.597-602. ⟨hal-00917868⟩

Olivier Hermant, James Lipton. Cut Elimination in the Intuitionistic Theory of Types with Axioms and Rewriting Cuts, Constructively. Studies in Logic and te Foundations of Mathematics, 2008, pp 101-134. ⟨hal-00912791⟩

Olivier Hermant, James Lipton. Eliminating Cuts in hoI(C ) - Extended Abstract. TEASE-LP: Workshop on Trends, Extensions, Applications and Semantics of Logic Programming, May 2020, Paris, France. ⟨hal-02958328⟩

Frédéric Blanqui, Guillaume Genestier, Olivier Hermant. Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting. FSCD 2019 - 4th International Conference on Formal Structures for Computation and Deduction, Jun 2019, Dortmund, Germany. ⟨10.4230/LIPIcs.FSCD.2019.9⟩. ⟨hal-01943941v4⟩

Frédéric Blanqui, Guillaume Genestier, Olivier Hermant. Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting. TYPES 2019 - 25th International Conference on Types for Proofs and Programs, Jun 2019, Oslo, Norway. pp.30-31. ⟨hal-02442484⟩

Thomas Pasquier, Xueyuan Han, Thomas Moyer, Adam Bates, Olivier Hermant, et al.. Runtime Analysis of Whole-System Provenance. The 25th ACM Conference on Computer and Communications Security, Oct 2018, Toronto, Canada. pp.1601-1616. ⟨hal-01859773⟩

Olivier Hermant. Polarized Rewriting and Tableaux in B Set Theory. 3RD INTERNATIONAL WORKSHOP ABOUT SETS AND TOOLS (SETS 2018), Jun 2018, Southampton, United Kingdom. pp.67-72. ⟨hal-01820522⟩

Olivier Hermant. Not Incompatible Logics. the GI-Dagstuhl Seminars : Universality of Proofs, Oct 2016, Dagstuhl, Germany. ⟨hal-01463138⟩

Ali Assaf, Guillaume Burel, Raphal Cauderlier, David Delahaye, Gilles Dowek, et al.. Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system. TYPES: Types for Proofs and Programs, May 2016, Novi SAd, Serbia. ⟨hal-01441751⟩

Thomas Pasquier, Jatinder Singh, Jean Bacon, Olivier Hermant. Managing Big Data with Information Flow Control. 8th IEEE International Conference on Cloud Computing (CLOUD 2015), Jun 2015, New York, United States. ⟨hal-01260014⟩

Emilio Jesús Gallego Arias, Olivier Hermant, Pierre Jouvelot. Verification of Faust Signal Processing Programs in COQ. The 1st International Workshop on Coq for PL (Co-located with POPL), Jan 2015, Mumbai, India. ⟨hal-01108173⟩

Emilio Jesús Gallego Arias, Olivier Hermant, Pierre Jouvelot. A Taste of Sound Reasoning in Faust. The Linux Audio Conference (LAC 2015) , Johannes Gutenberg University (JGU), Apr 2015, Mainz, Germany. ⟨hal-01251069⟩

Olivier Hermant, Vivien Maisonneuve. Des réels aux flottants : préservation automatique de preuves de stabilité de Lyapunov. AFADL, Pascale Le Gall; Frederic Dadeau, Jun 2015, Bordeaux, France. pp.51-56. ⟨hal-01138327⟩

Gaëtan Gilbert, Olivier Hermant. Normalization by Completeness with Heyting Algebras. LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji. ⟨hal-01204599⟩

Guillaume Bury, David Delahaye, Damien Doligez, Pierre Halmagrand, Olivier Hermant. Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo. LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji. pp 42-58. ⟨hal-01204701v2⟩

Vivien Maisonneuve, Olivier Hermant, François Irigoin. ALICe: A Framework to Improve Affine Loop Invariant Computation . the 5th International Workshop on Invariant Generation (WING 2014), Jul 2014, Vienne, Austria. ⟨hal-01086957⟩

Vivien Maisonneuve, Olivier Hermant, François Irigoin. Computing Invariants with Transformers: Experimental Scalability and Accuracy. Fifth International Workshop on Numerical and Symbolic Abstract Domains, Sep 2014, Munich, Germany. 14 p., Pages 17-31, ⟨10.1016/j.entcs.2014.08.003⟩. ⟨hal-01058298⟩

Lisa Allali, Olivier Hermant. Semantic A-translation and Super-consistency entail Classical Cut Elimination. LPAR 19 - 19th Conference on Logic for Programming, Artificial Intelligence, and Reasoning - 2013, Bernd Fischer, Geoff Sutcliffe, Dec 2013, Stellenbosch, South Africa. pp.407-422, ⟨10.1007/978-3-642-45221-5_28⟩. ⟨hal-00923915⟩

Mélanie Boudard, Olivier Hermant. Polarizing Double Negation Translations. LPAR, Dec 2013, Stellenbosch, South Africa. pp.182-197. ⟨hal-00920224v2⟩

Truong Giang Le, Dmitriy Fedosov, Olivier Hermant, Matthieu Manceny, Renaud Pawlak, et al.. Programming Robots With Events. 4th International Embedded Systems Symposium (IESS), Jun 2013, Paderborn, Germany. pp.14-25, ⟨10.1007/978-3-642-38853-8_2⟩. ⟨hal-00924489⟩

David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant. Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo. LPAR - Logic for Programming Artificial Intelligence and Reasoning - 2013, Dec 2013, Stellenbosch, South Africa. pp.274-290, ⟨10.1007/978-3-642-45221-5_20⟩. ⟨hal-00909784⟩

David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant. Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps. IWIL - 10th International Workshop on the Implementation of Logics - 2013, Dec 2013, Stellenbosch, South Africa. ⟨hal-00909688⟩

Truong Giang Le, Olivier Hermant, Matthieu Manceny, Renaud Pawlak, Renaud Rioboo. Using Event-Based Style for Developing M2M Applications. GPC - 8th International Conference on Grid and Pervasive Computing - 2013, 2013, Seoul, South Korea. pp.348-357, ⟨10.1007/978-3-642-38027-3_37⟩. ⟨hal-00924491⟩

Mathieu Boespflug, Quentin Carbonneaux, Olivier Hermant, Ronan Saillard. Dedukti: A Universal Proof Checker. Journées communes LTP - LAC, Oct 2012, Orléans, France. ⟨hal-01537578⟩

Ksenia Khramenkova, Olivier Hermant, Renaud Pawlak. Simulator Of A "Weather" Cloud. 10th Finnish-Russian University Cooperation in Telecommunication Workshop (FRUCT), Apr 2012, St.-Petersburg, Russia. ⟨hal-00909649⟩

Mathieu Boespflug, Quentin Carbonneaux, Olivier Hermant. The λΠ-calculus Modulo as a Universal Proof Language. the Second International Workshop on Proof Exchange for Theorem Proving (PxTP 2012), Jun 2012, Manchester, United Kingdom. pp. 28-43. ⟨hal-00917845⟩

Denis Cousineau, Olivier Hermant. A Semantic Proof that Reducibility Candidates entail Cut Elimination. RTA'12 - 23rd International Conference on Rewriting Techniques and Applications, May 2012, Nagoya, Japan. pp.133--148, ⟨10.4230/LIPIcs.RTA.2012.133⟩. ⟨hal-00743284⟩

Giang Le Truong, Olivier Hermant, Matthieu Manceny, Renaud Pawlak, Renaud Rioboo. Unifying Event-based and Rule-based Styles to Develop Concurrent and Context-aware Reactive Applications - Toward a Convenient Support for Concurrent and Reactive Program. International Conference on Software Paradigm Trends, Jul 2012, Rome, Italy. pp.347-350. ⟨hal-01126209⟩

Truong Giang Le, Olivier Hermant, Matthieu Manceny, Renaud Pawlak, Renaud Rioboo. Unifying Event-based and Rule-based Styles for Concurrent and Reactive Applications. The 7th International Conference on Software Paradigm Trends, ICSOFT 2012, Jul 2012, Rome, Italy. pp.347-350. ⟨hal-00829701⟩

Truong Giang Le, Olivier Hermant, Matthieu Manceny, Renaud Pawlak. Dynamic Adaptation through Event Recon guration. Workshop on Variability, Adaptation and Dynamism in software systEms and seRvices (VADER 2011), Oct 2011, Hersonissos, Crete, Greece. ⟨hal-00909684⟩

Truong Giang Le, Olivier Hermant, Matthieu Manceny, Renaud Pawlak. Dynamic Adaptation through Event Reconfiguration. Variability, Adaptation and Dynamism in software systEms and seRvices (VADER 2011), Oct 2011, Hersonissos, Crete, France. pp.637-646. ⟨hal-00639556⟩

Olivier Hermant, James Lipton. A constructive semantic approach to cut elimination in type theories with axiom. 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Sep 2008, Bertinoro, Italy. pp 169-183, ⟨10.1007/978-3-540-87531-4_14⟩. ⟨hal-00916025⟩

Gilles Dowek, Olivier Hermant. A simple proof that super consistency implies cut elimination. 18th International Conference, RTA 2007, Jun 2007, Paris, France. pp.Pages 93-106, ⟨10.1007/978-3-540-73449-9_9⟩. ⟨hal-00743256⟩

Sathiya Prabhu Kumar, Sylvain Lefebvre, Raja Chiky, Olivier Hermant. Consistency-Latency Trade-Off of the LibRe Protocol: A Detailed Study. Advances in Knowledge Discovery and Management, 7, Springer, pp.83-108, 2018, ⟨10.1007/978-3-319-65406-5_4⟩. ⟨hal-02066058⟩

Richard Bonichon, Olivier Hermant. A syntactic soundness proof for free-variable tableaux with on-the-fly Skolemization. 2015. ⟨hal-01154799⟩

Alois Brunel, Olivier Hermant, Clement Houtmann. Orthogonality and Boolean Algebras for Deduction Modulo. 2011. ⟨inria-00563331⟩

Gilles Dowek, Olivier Hermant. A simple proof that super-consistency implies cut elimination. 2007. ⟨hal-00150697⟩

Vivien Maisonneuve, Olivier Hermant, François Irigoin. Preservation of Lyapunov-Theoretic Proofs: From Real to Floating-Point Arithmetic. [Research Report] Mines ParisTech. 2014. ⟨hal-01086732⟩

Olivier Hermant. Complétude en Logiques. Informatique [cs]. Université Paris Diderot (Paris 7), 2017. ⟨tel-01529422⟩