Suivre
Olivier Hermant
Olivier Hermant
CRI, MINES ParisTech
Adresse e-mail validée de inria.fr - Page d'accueil
Titre
Citée par
Citée par
Année
The λΠ-calculus Modulo as a Universal Proof Language.
M Boespflug, Q Carbonneaux, O Hermant
PxTP, 28-43, 2012
952012
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
732018
Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
D Delahaye, D Doligez, F Gilbert, P Halmagrand, O Hermant
Logic for Programming, Artificial Intelligence, and Reasoning: 19th …, 2013
472013
Semantic cut elimination in the intuitionistic sequent calculus
O Hermant
Typed Lambda Calculi and Applications: 7th International Conference, TLCA …, 2005
402005
Méthodes sémantiques en déduction modulo
O Hermant
Doctoral Thesis. Université de Paris 7, 2005
292005
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
232016
Resolution is cut-free
O Hermant
Journal of Automated Reasoning 44, 245-276, 2010
232010
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
212015
A semantic completeness proof for TaMed
R Bonichon, O Hermant
Logic for Programming, Artificial Intelligence, and Reasoning: 13th …, 2006
212006
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
202016
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
172019
A model-based cut elimination proof
O Hermant
2nd St-Petersburg Days of Logic and Computability 972, 2003
152003
Dependency pairs termination in dependent type theory modulo rewriting
F Blanqui, G Genestier, O Hermant
arXiv preprint arXiv:1906.11649, 2019
142019
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
142007
On constructive cut admissibility in deduction modulo
R Bonichon, O Hermant
Types for Proofs and Programs: International Workshop, TYPES 2006 …, 2007
142007
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
102019
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
92020
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
92015
Computing invariants with transformers: experimental scalability and accuracy
V Maisonneuve, O Hermant, F Irigoin
Electronic Notes in Theoretical Computer Science 307, 17-31, 2014
92014
Le système ne peut pas réaliser cette opération maintenant. Veuillez réessayer plus tard.
Articles 1–20