Accéder directement au contenu

Olivier Hermant

44
Documents

Présentation

Olivier HERMANT [CRI](http://cri.mines-paristech.fr) Mines ParisTech 35 rue Saint-Honoré 77 305 Fontainebleau (France) Tel: +33 (0)1 64 69 48 31
Olivier HERMANT [CRI](http://cri.mines-paristech.fr) Mines ParisTech 35 rue Saint-Honoré 77 305 Fontainebleau (France) Tel: +33 (0)1 64 69 48 31

Publications

Image document

Eliminating Cuts in hoI(C ) - Extended Abstract

Olivier Hermant , James Lipton
TEASE-LP: Workshop on Trends, Extensions, Applications and Semantics of Logic Programming, May 2020, Paris, France
Communication dans un congrès hal-02958328v1
Image document

Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting

Frédéric Blanqui , Guillaume Genestier , Olivier Hermant
FSCD 2019 - 4th International Conference on Formal Structures for Computation and Deduction, Jun 2019, Dortmund, Germany. ⟨10.4230/LIPIcs.FSCD.2019.9⟩
Communication dans un congrès hal-01943941v4
Image document

Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting

Frédéric Blanqui , Guillaume Genestier , Olivier Hermant
TYPES 2019 - 25th International Conference on Types for Proofs and Programs, Jun 2019, Oslo, Norway. pp.30-31
Communication dans un congrès hal-02442484v1

Runtime Analysis of Whole-System Provenance

Thomas Pasquier , Xueyuan Han , Thomas Moyer , Adam Bates , Olivier Hermant
The 25th ACM Conference on Computer and Communications Security, Oct 2018, Toronto, Canada. pp.1601-1616
Communication dans un congrès hal-01859773v1
Image document

Polarized Rewriting and Tableaux in B Set Theory

Olivier Hermant
3RD INTERNATIONAL WORKSHOP ABOUT SETS AND TOOLS (SETS 2018), Jun 2018, Southampton, United Kingdom. pp.67-72
Communication dans un congrès hal-01820522v1
Image document

Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system

Ali Assaf , Guillaume Burel , Raphal Cauderlier , David Delahaye , Gilles Dowek
TYPES: Types for Proofs and Programs, May 2016, Novi SAd, Serbia
Communication dans un congrès hal-01441751v1

Not Incompatible Logics

Olivier Hermant
the GI-Dagstuhl Seminars : Universality of Proofs, Oct 2016, Dagstuhl, Germany
Communication dans un congrès hal-01463138v1
Image document

Verification of Faust Signal Processing Programs in COQ

Emilio Jesús Gallego Arias , Olivier Hermant , Pierre Jouvelot
The 1st International Workshop on Coq for PL (Co-located with POPL), Jan 2015, Mumbai, India
Communication dans un congrès hal-01108173v1
Image document

Managing Big Data with Information Flow Control

Thomas Pasquier , Jatinder Singh , Jean Bacon , Olivier Hermant
8th IEEE International Conference on Cloud Computing (CLOUD 2015), Jun 2015, New York, United States
Communication dans un congrès hal-01260014v1
Image document

Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo

Guillaume Bury , David Delahaye , Damien Doligez , Pierre Halmagrand , Olivier Hermant
LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji. pp 42-58
Communication dans un congrès hal-01204701v2
Image document

Des réels aux flottants : préservation automatique de preuves de stabilité de Lyapunov

Olivier Hermant , Vivien Maisonneuve
AFADL, Pascale Le Gall; Frederic Dadeau, Jun 2015, Bordeaux, France. pp.51-56
Communication dans un congrès hal-01138327v1
Image document

A Taste of Sound Reasoning in Faust

Emilio Jesús Gallego Arias , Olivier Hermant , Pierre Jouvelot
The Linux Audio Conference (LAC 2015) , Johannes Gutenberg University (JGU), Apr 2015, Mainz, Germany
Communication dans un congrès hal-01251069v1
Image document

Normalization by Completeness with Heyting Algebras

Gaëtan Gilbert , Olivier Hermant
LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji
Communication dans un congrès hal-01204599v1
Image document

ALICe: A Framework to Improve Affine Loop Invariant Computation

Vivien Maisonneuve , Olivier Hermant , François Irigoin
the 5th International Workshop on Invariant Generation (WING 2014), Jul 2014, Vienne, Austria
Communication dans un congrès hal-01086957v1
Image document

Computing Invariants with Transformers: Experimental Scalability and Accuracy

Vivien Maisonneuve , Olivier Hermant , François Irigoin
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⟩
Communication dans un congrès hal-01058298v1
Image document

Using Event-Based Style for Developing M2M Applications

Truong Giang Le , Olivier Hermant , Matthieu Manceny , Renaud Pawlak , Renaud Rioboo
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⟩
Communication dans un congrès hal-00924491v1
Image document

Programming Robots With Events

Truong Giang Le , Dmitriy Fedosov , Olivier Hermant , Matthieu Manceny , Renaud Pawlak
4th International Embedded Systems Symposium (IESS), Jun 2013, Paderborn, Germany. pp.14-25, ⟨10.1007/978-3-642-38853-8_2⟩
Communication dans un congrès hal-00924489v1
Image document

Polarizing Double Negation Translations

Mélanie Boudard , Olivier Hermant
LPAR, Dec 2013, Stellenbosch, South Africa. pp.182-197
Communication dans un congrès hal-00920224v2
Image document

Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo

David Delahaye , Damien Doligez , Frédéric Gilbert , Pierre Halmagrand , Olivier Hermant
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⟩
Communication dans un congrès hal-00909784v1
Image document

Semantic A-translation and Super-consistency entail Classical Cut Elimination

Lisa Allali , Olivier Hermant
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⟩
Communication dans un congrès hal-00923915v1
Image document

Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps

David Delahaye , Damien Doligez , Frédéric Gilbert , Pierre Halmagrand , Olivier Hermant
IWIL - 10th International Workshop on the Implementation of Logics - 2013, Dec 2013, Stellenbosch, South Africa
Communication dans un congrès hal-00909688v1
Image document

The λΠ-calculus Modulo as a Universal Proof Language

Mathieu Boespflug , Quentin Carbonneaux , Olivier Hermant
the Second International Workshop on Proof Exchange for Theorem Proving (PxTP 2012), Jun 2012, Manchester, United Kingdom. pp. 28-43
Communication dans un congrès hal-00917845v1

Unifying Event-based and Rule-based Styles for Concurrent and Reactive Applications

Truong Giang Le , Olivier Hermant , Matthieu Manceny , Renaud Pawlak , Renaud Rioboo
The 7th International Conference on Software Paradigm Trends, ICSOFT 2012, Jul 2012, Rome, Italy. pp.347-350
Communication dans un congrès hal-00829701v1

Dedukti: A Universal Proof Checker

Mathieu Boespflug , Quentin Carbonneaux , Olivier Hermant , Ronan Saillard
Journées communes LTP - LAC, Oct 2012, Orléans, France
Communication dans un congrès hal-01537578v1

Unifying Event-based and Rule-based Styles to Develop Concurrent and Context-aware Reactive Applications - Toward a Convenient Support for Concurrent and Reactive Program

Giang Le Truong , Olivier Hermant , Matthieu Manceny , Renaud Pawlak , Renaud Rioboo
International Conference on Software Paradigm Trends, Jul 2012, Rome, Italy. pp.347-350
Communication dans un congrès hal-01126209v1
Image document

Simulator Of A "Weather" Cloud

Ksenia Khramenkova , Olivier Hermant , Renaud Pawlak
10th Finnish-Russian University Cooperation in Telecommunication Workshop (FRUCT), Apr 2012, St.-Petersburg, Russia
Communication dans un congrès hal-00909649v1
Image document

A Semantic Proof that Reducibility Candidates entail Cut Elimination

Denis Cousineau , Olivier Hermant
RTA'12 - 23rd International Conference on Rewriting Techniques and Applications, May 2012, Nagoya, Japan. pp.133--148, ⟨10.4230/LIPIcs.RTA.2012.133⟩
Communication dans un congrès hal-00743284v1
Image document

Dynamic Adaptation through Event Recon guration

Truong Giang Le , Olivier Hermant , Matthieu Manceny , Renaud Pawlak
Workshop on Variability, Adaptation and Dynamism in software systEms and seRvices (VADER 2011), Oct 2011, Hersonissos, Crete, Greece
Communication dans un congrès hal-00909684v1
Image document

Dynamic Adaptation through Event Reconfiguration

Truong Giang Le , Olivier Hermant , Matthieu Manceny , Renaud Pawlak
Variability, Adaptation and Dynamism in software systEms and seRvices (VADER 2011), Oct 2011, Hersonissos, Crete, France. pp.637-646
Communication dans un congrès hal-00639556v1

A constructive semantic approach to cut elimination in type theories with axiom

Olivier Hermant , James Lipton
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⟩
Communication dans un congrès hal-00916025v1
Image document

A simple proof that super consistency implies cut elimination

Gilles Dowek , Olivier Hermant
18th International Conference, RTA 2007, Jun 2007, Paris, France. pp.Pages 93-106, ⟨10.1007/978-3-540-73449-9_9⟩
Communication dans un congrès hal-00743256v1
Image document

Complétude en Logiques

Olivier Hermant
Informatique [cs]. Université Paris Diderot (Paris 7), 2017
HDR tel-01529422v1