The λΠ-calculus modulo as a universal proof language M Boespflug, Q Carbonneaux, O Hermant Proceedings of PxTP2012: Proof Exchange for Theorem Proving, 28-43, 2012 | 94 | 2012 |

*Zenon Modulo:* When Achilles Outruns the Tortoise Using Deduction ModuloD Delahaye, D Doligez, F Gilbert, P Halmagrand, O Hermant International Conference on Logic for Programming Artificial Intelligence …, 2013 | 46 | 2013 |

Runtime analysis of whole-system provenance T Pasquier, X Han, T Moyer, A Bates, O Hermant, D Eyers, J Bacon, ... Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications …, 2018 | 43 | 2018 |

Semantic cut elimination in the intuitionistic sequent calculus O Hermant International Conference on Typed Lambda Calculi and Applications, 221-233, 2005 | 39 | 2005 |

Méthodes sémantiques en déduction modulo O Hermant Doctoral Thesis. Université de Paris 7, 2005 | 29 | 2005 |

Resolution is cut-free O Hermant Journal of Automated Reasoning 44 (3), 245-276, 2010 | 24 | 2010 |

A semantic completeness proof for TaMed R Bonichon, O Hermant International Conference on Logic for Programming Artificial Intelligence …, 2006 | 21 | 2006 |

Dedukti: a logical framework based on the λΠ-calculus modulo theory A Assaf, G Burel, R Cauderlier, D Delahaye, G Dowek, C Dubois, F Gilbert, ... Manuscript http://www. lsv. fr/~ dowek/Publi/expressing. pdf, 2016 | 20 | 2016 |

Automated deduction in the B set theory using typed proof search and deduction modulo G Bury, D Delahaye, D Doligez, P Halmagrand, O Hermant LPAR 20: 20th International Conference on Logic for Programming, Artificial …, 2015 | 20 | 2015 |

Dedukti: a logical framework based on the λ Π-calculus modulo theory, 2016 A Assaf, G Burel, R Cauderlier, D Delahaye, G Dowek, C Dubois, F Gilbert, ... URL: http://www. lsv. fr/~ dowek/Publi/expressing. pdf, 2019 | 17 | 2019 |

Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system A Assaf, G Burel, R Cauderlier, D Delahaye, G Dowek, C Dubois, F Gilbert, ... 22nd International Conference on Types for Proofs and Programs, 2016 | 15 | 2016 |

A model-based cut elimination proof O Hermant 2nd St-Petersburg Days of Logic and Computability 972, 2003 | 15 | 2003 |

A simple proof that super-consistency implies cut elimination G Dowek, O Hermant Notre Dame Journal of Formal Logic 53 (4), 439-456, 2012 | 14* | 2012 |

A simple proof that super-consistency implies cut elimination G Dowek, O Hermant International Conference on Rewriting Techniques and Applications, 93-106, 2007 | 14 | 2007 |

On constructive cut admissibility in deduction modulo R Bonichon, O Hermant International Workshop on Types for Proofs and Programs, 33-47, 2006 | 14 | 2006 |

Dependency pairs termination in dependent type theory modulo rewriting F Blanqui, G Genestier, O Hermant arXiv preprint arXiv:1906.11649, 2019 | 10 | 2019 |

Computing invariants with transformers: experimental scalability and accuracy V Maisonneuve, O Hermant, F Irigoin Electronic Notes in Theoretical Computer Science 307, 17-31, 2014 | 8 | 2014 |

Dedukti: a Logical Framework based on the lambda-pi-Calculus Modulo Theory. draft A Assaf, G Burel, R Cauderlier, G Dowek, C Dubois, F Gilbert, ... INRIA, 2019 | 7 | 2019 |

Managing big data with information flow control TFJM Pasquier, J Singh, J Bacon, O Hermant 2015 IEEE 8th International Conference on Cloud Computing, 524-531, 2015 | 7 | 2015 |

Polarizing double-negation translations M Boudard, O Hermant International Conference on Logic for Programming Artificial Intelligence …, 2013 | 7 | 2013 |