Nombre de documents

36


Olivier HERMANT

CRI
Mines ParisTech
35 rue Saint-Honoré
77 305 Fontainebleau (France)
Tel: +33 (0)1 64 69 48 31


Article dans une revue4 documents

  • 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, 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. 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. 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〉

Communication dans un congrès27 documents

  • Olivier Hermant. Not Incompatible Logics. the GI-Dagstuhl Seminars : Universality of Proofs, Oct 2016, Dagstuhl, Germany. 〈http://www.dagstuhl.de/de/programm/kalender/semhp/?semnr=16421〉. 〈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. 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 2016, Novi SAd, Serbia. 〈hal-01441751〉
  • Emilio Jesús Gallego Arias, Olivier Hermant, Pierre Jouvelot. A Taste of Sound Reasoning in Faust. The Linux Audio Conference (LAC 2015) , Apr 2015, Mainz, Germany. 〈http://lac.linuxaudio.org/2015/〉. 〈hal-01251069〉
  • 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〉
  • 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〉
  • Thomas F. J.-M. 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〉
  • Olivier Hermant, Vivien Maisonneuve. Des réels aux flottants : préservation automatique de preuves de stabilité de Lyapunov. AFADL, Jun 2015, Bordeaux, France. pp.51-56, Approches Formelles dans l'Assistance au Développement Logiciel. 〈hal-01138327〉
  • 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. Vol. 307, 14 p., Pages 17-31, 2014, 〈10.1016/j.entcs.2014.08.003〉. 〈hal-01058298〉
  • Truong Giang Le, Olivier Hermant, Matthieu Manceny, Renaud Pawlak, Renaud Rioboo. Using Event-based Style for Developing M2M Applications. Proceedings of The 8th International Conference on Grid and Pervasive Computing, Lecture Notes in Computer Science, Volume 7861, May 2013, Seoul, South Korea. 7861, pp.348-357, 2013. 〈hal-00829759〉
  • Lisa Allali, Olivier Hermant. Semantic A-translation and Super-consistency entail Classical Cut Elimination. Ken McMillan and Aart Middeldorp and Andrei Voronkov. LPAR 19 - 19th Conference on Logic for Programming, Artificial Intelligence, and Reasoning - 2013, Dec 2013, Stellenbosch, South Africa. Springer, 8312, pp.407-422, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-45221-5_28〉. 〈hal-00923915〉
  • Truong Giang Le, Olivier Hermant, Matthieu Manceny, Renaud Pawlak, Renaud Rioboo. Using Event-Based Style for Developing M2M Applications. James Park and Hamid Arabnia and Cheonshik Kim and Weisong Shi and Joon-Min Gil. GPC - 8th International Conference on Grid and Pervasive Computing - 2013, 2013, Seoul, South Korea. Springer, 7861, pp.348-357, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-38027-3_37〉. 〈hal-00924491〉
  • Truong Giang Le, Dmitriy Fedosov, Olivier Hermant, Matthieu Manceny, Renaud Pawlak, et al.. Programming Robots With Events. Gunar Schirner; Marcelo Götz; Achim Rettberg; Mauro C. Zanella; Franz J. Rammig. 4th International Embedded Systems Symposium (IESS), Jun 2013, Paderborn, Germany. Springer, IFIP Advances in Information and Communication Technology, AICT-403, pp.14-25, 2013, Embedded Systems: Design, Analysis and Verification. 〈10.1007/978-3-642-38853-8_2〉. 〈hal-00924489〉
  • 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. Stephan Schulz and Geoff Sutcliffe and Boris Konev. IWIL - 10th International Workshop on the Implementation of Logics - 2013, Dec 2013, Stellenbosch, South Africa. EasyChair, 2013. 〈hal-00909688〉
  • David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant. Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo. Ken McMillan and Aart Middeldorp and Andrei Voronkov. LPAR - Logic for Programming Artificial Intelligence and Reasoning - 2013, Dec 2013, Stellenbosch, South Africa. Springer, 8312, pp.274-290, 2013, LNCS. 〈10.1007/978-3-642-45221-5_20〉. 〈hal-00909784〉
  • Mélanie Boudard, Olivier Hermant. Polarizing Double Negation Translations. Ken McMillan and Aart Middeldorp and Andrei Voronkov. LPAR, Dec 2013, Stellenbosch, South Africa. Springer, 8312, pp.182-197, 2013, LNCS ARCoSS. 〈hal-00920224v2〉
  • 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, 2012. 〈hal-00829701〉
  • 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, 2012. 〈hal-01126209〉
  • 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〉
  • Mathieu Boespflug, Quentin Carbonneaux, Olivier Hermant. The λΠ-calculus Modulo as a Universal Proof Language. David Pichardie, Tjark Weber. the Second International Workshop on Proof Exchange for Theorem Proving (PxTP 2012), Jun 2012, Manchester, United Kingdom. Vol. 878, pp. 28-43, 2012. 〈hal-00917845〉
  • 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〉
  • Denis Cousineau, Olivier Hermant. A Semantic Proof that Reducibility Candidates entail Cut Elimination. 23rd International Conference on Rewriting Techniques and Applications (RTA'12), May 2012, Nagoya, Japan. 15, pp.133--148, 2012, 〈10.4230/LIPIcs.RTA.2012.133〉. 〈hal-00743284〉
  • 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. Gerhard Goos, Juris Hartmanis, and Jan van Leeuwen. Variability, Adaptation and Dynamism in software systEms and seRvices (VADER 2011), Oct 2011, Hersonissos, Crete, France. Springer, pp.637-646, 2011, Lecture Notes in Computer Science. 〈hal-00639556〉
  • Olivier Hermant, James Lipton. A constructive semantic approach to cut elimination in type theories with axiom. Springer-Verlag Berlin Heidelberg. 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Sep 2008, Bertinoro, Italy. Springer Berlin Heidelberg, 5213, pp 169-183, 2008, 0302-9743. 〈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. 4533, pp.Pages 93-106, 2007, 〈10.1007/978-3-540-73449-9_9〉. 〈hal-00743256〉

Pré-publication, Document de travail3 documents

  • 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〉

Rapport1 document

  • 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〉

HDR1 document

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