Folgen
Olivier Hermant
Olivier Hermant
CRI, MINES ParisTech
Bestätigte E-Mail-Adresse bei inria.fr - Startseite
Titel
Zitiert von
Zitiert von
Jahr
The λΠ-calculus Modulo as a Universal Proof Language.
M Boespflug, Q Carbonneaux, O Hermant
PxTP, 28-43, 2012
962012
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
722018
Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
D Delahaye, D Doligez, F Gilbert, P Halmagrand, O Hermant
International Conference on Logic for Programming Artificial Intelligence …, 2013
482013
Semantic cut elimination in the intuitionistic sequent calculus
O Hermant
International Conference on Typed Lambda Calculi and Applications, 221-233, 2005
402005
Méthodes sémantiques en déduction modulo
O Hermant
Doctoral Thesis. Université de Paris 7, 2005
292005
Resolution is cut-free
O Hermant
Journal of Automated Reasoning 44 (3), 245-276, 2010
242010
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
222016
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 (short papers), 42-58, 2015
222015
A semantic completeness proof for TaMed
R Bonichon, O Hermant
International Conference on Logic for Programming Artificial Intelligence …, 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. Novi SAd, Serbia (May 2016), 2016
182016
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
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
International Workshop on Types for Proofs and Programs, 33-47, 2006
142006
Dependency pairs termination in dependent type theory modulo rewriting
F Blanqui, G Genestier, O Hermant
arXiv preprint arXiv:1906.11649, 2019
132019
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
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
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 (6), 1001-1050, 2020
82020
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
82015
Das System kann den Vorgang jetzt nicht ausführen. Versuchen Sie es später erneut.
Artikel 1–20