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 | 100 | 2018 |

The λΠ-calculus Modulo as a Universal Proof Language. M Boespflug, Q Carbonneaux, O Hermant PxTP, 28-43, 2012 | 97 | 2012 |

*Zenon Modulo:* When Achilles Outruns the Tortoise Using Deduction ModuloD Delahaye, D Doligez, F Gilbert, P Halmagrand, O Hermant Logic for Programming, Artificial Intelligence, and Reasoning: 19th …, 2013 | 47 | 2013 |

Semantic cut elimination in the intuitionistic sequent calculus O Hermant Typed Lambda Calculi and Applications: 7th International Conference, TLCA …, 2005 | 42 | 2005 |

Dedukti: a logical framework based on the λΠ-calculus modulo theory A Assaf, G Burel, R Cauderlier, D Delahaye, G Dowek, C Dubois, F Gilbert, ... | 33 | 2016 |

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

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, ... TYPES: Types for Proofs and Programs, 2016 | 25 | 2016 |

Resolution is cut-free O Hermant Journal of Automated Reasoning 44, 245-276, 2010 | 23 | 2010 |

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 | 22 | 2015 |

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, 2019 A Assaf, G Burel, R Cauderlier, D Delahaye, G Dowek, C Dubois, F Gilbert, ... URL: http://www. lsv. fr/~ dowek/Publi/expressing. pdf, 2019 | 20 | 2019 |

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

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

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

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

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

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 | 12 | 2015 |

First-order automated reasoning with theories: when deduction modulo theory meets practice G Burel, G Bury, R Cauderlier, D Delahaye, P Halmagrand, O Hermant Journal of Automated Reasoning 64, 1001-1050, 2020 | 11 | 2020 |

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

Polarizing double-negation translations M Boudard, O Hermant Logic for Programming, Artificial Intelligence, and Reasoning: 19th …, 2013 | 7 | 2013 |