@inProceedings{OHer05,
author = {Olivier Hermant},
title = {Semantic cut elimination in the Intuitionistic Sequent Calculus},
year = {2005},
booktitle = {Typed Lambda-Calculi and Applications},
address = {Nara, Japan},
editor = {Pawel Urzyczyn},
series = {Lecture Notes in Computer Science}
volume = {3461},
publisher = {Springer-Verlag},
pages = {221-233}
}
@Article{OHer03,
author = {Olivier Hermant},
title = {A Model-based Cut Elimination Proof},
year = {2003},
journal = {2nd St-Petersburg Days of Logic and Computability},
address = {Saint-Petersburg, Russia}
}
@inProceedings{RBonOHer06a,
author = {Richard Bonichon and Olivier Hermant},
title = {A semantic completeness proof for TaMeD},
year = {2006},
booktitle = {LPAR},
address = {Phnom Penh, Cambodia},
series = {LNCS},
volume = {4246},
publisher={Springer-Verlag},
pages={167-181}
}
@InProceedings{RBonOHer06b,
author = {Richard Bonichon and Olivier Hermant},
title = {On Constructive Cut Admissibility in Deduction Modulo},
pages = {33-47},
crossref = {Proc/types06}
}
@proceedings{Proc/types06,
editor = {Thorsten Altenkirch and Conor McBride},
title = {International Workshop TYPES 2006, Nottingham, UK,
April 18-21, 2006, Revised Selected Papers},
booktitle = {TYPES for proofs and programs},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4502},
year = {2007},
isbn = {978-3-540-74463-4},
issn = {0302-9743 (Print) 1611-3349 (Online)}
}
@inproceedings{GDowOHer07,
author = {Gilles Dowek and Olivier Hermant},
title = {A Simple Proof That Super-Consistency Implies Cut
Elimination},
booktitle = {RTA},
year = {2007},
pages = {93-106},
ee = {http://dx.doi.org/10.1007/978-3-540-73449-9_9},
crossref = {DBLP:conf/rta/2007}
}
@proceedings{DBLP:conf/rta/2007,
editor = {Franz Baader},
title = {Term Rewriting and Applications, 18th
International Conference, RTA 2007, Paris, France, June 26-28, 2007,
Proceedings},
booktitle = {RTA},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4533},
year = {2007},
isbn = {978-3-540-73447-5}
}
@Article{OHer08a,
author = {Hermant, Olivier},
title = {Skolemization in various intuitionistic logics},
year={2008},
note={To appear},
publisher={Springer},
journal={Archive for Mathematical Logic}
}
@InCollection{OHerJLip08a,
author = {Olivier Hermant and James Lipton},
booktitle = {Festschrift in Honor of Peter B. Andrews on His 70th
Birthday},
title = {Cut Elimination in the Intuitionistic Theory of Types with
Axioms and Rewriting Cuts, Constructively},
publisher = {IFCoLog},
year = 2008,
series = {Studies in Logic and the Foundations of Mathematics},
EDITOR = {Benzm{u}ller, C. E. and Brown, C. E. and Siekmann, J. and
Statman, R.}
}
@article{DBLP:OHerJLip10,
author = {Olivier Hermant and
James Lipton},
title = {Completeness and Cut-elimination in the Intuitionistic Theory
of Types - Part 2},
journal = {J. Log. Comput.},
volume = {20},
number = {2},
year = {2010},
pages = {597-602},
ee = {http://dx.doi.org/10.1093/logcom/exp076},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{OHerJLip08c,
author = {Olivier Hermant and
James Lipton},
title = {A Constructive Semantic Approach to Cut Elimination in Type
Theories with Axioms},
booktitle = {CSL},
year = {2008},
pages = {169-183},
ee = {http://dx.doi.org/10.1007/978-3-540-87531-4_14},
crossref = {DBLP:conf/csl/2008},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/csl/2008,
editor = {Michael Kaminski and
Simone Martini},
title = {Computer Science Logic, 22nd International Workshop, CSL
2008, 17th Annual Conference of the EACSL, Bertinoro, Italy,
September 16-19, 2008. Proceedings},
booktitle = {CSL},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5213},
year = {2008},
isbn = {978-3-540-87530-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@Article{OHer10,
author = "Hermant, Olivier",
title = "Resolution is Cut-Free",
journal = "Journal of Automated Reasoning",
volume = "44",
number = "3",
month = "March",
year = "2010",
pages = "245-276"
}
@inproceedings{ABruOHerCHou11,
author = "Alo\"{i}s Brunel, Olivier Hermant and Cl\'ement Houtmann",
title = "Orthogonality and Boolean Algebras for Deduction Modulo",
booktitle = {TLCA},
year = "2011",
pages = {76-90}
crossref = {TLCA11}
}
@proceedings{TLCA11,
editor = {Luke Ong},
title = {Typed Lambda-Calculus and Applications Conference. Proceedings.},
booktitle = {TLCA},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6990},
year = {2011}
}
@Article{GDowOHer12,
author = "Dowek, Gilles and Hermant, Olivier",
title = "A Simple Proof that Super-Consistency implies Cut-Elimination",
journal = "Notre-Dame Journal of Formal Logic",
year = "2012",
volume = "53",
numer = "4",
pages = "439-456"
}
@inProceedings{MBoeQCarOHer12,
author = {Mathieu Boespflug and Quentin Carbonneaux and Olivier Hermant},
title = {The {$\lambda\Pi$}-calculus Modulo as a Universal Proof Language},
booltitle = {In Second Workshop on Proof Exchange for Theorem Proving (PxTP)},
publisher = {CEUR-WS.org},
volume = {878},
pages = {28-43},
url = {ceur-ws.org/Vol-878/paper2.pdf},
year = {2012}
}
@inproceedings{DCouOHer12,
author = {Denis Cousineau and
Olivier Hermant},
title = {A Semantic Proof that Reducibility Candidates entail Cut
Elimination},
booktitle = {RTA},
year = {2012},
pages = {133-148},
editor = {Ashish Tiwari},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
series = {LIPIcs},
volume = {15}
}
@inproceedings{GLTrOHerMManRPawRRio12,
author = {Truong Giang Le and
Olivier Hermant and
Matthieu Manceny and
Renaud Pawlak and
Renaud Rioboo},
title = {Unifying Event-based and Rule-based Styles to Develop Concurrent
and Context-aware Reactive Applications - Toward a Convenient
Support for Concurrent and Reactive Programming},
booktitle = {ICSOFT},
year = {2012},
pages = {347-350},
crossref = {icsoft2012}
}
@proceedings{icsoft2012,
editor = {Slimane Hammoudi and
Marten van Sinderen and
Jos{\'e} Cordeiro},
title = {ICSOFT 2012 - Proceedings of the 7th International Conference
on Software Paradigm Trends, Rome, Italy, 24 - 27 July,
2012},
booktitle = {ICSOFT},
publisher = {SciTePress},
year = {2012},
isbn = {978-989-8565-19-8}
}
@inproceedings{LAllOHer13,
author = {Lisa Allali and
Olivier Hermant},
title = {Semantic A-Translations and Super-Consistency entail
Classical Cut Elimination},
booktitle = {LPAR},
year = {2013},
pages = {407-422},
editor = {Ken McMillan and
Aart Middeldorp and
Andre{\"i} Voronkov},
publisher = {Springer},
series = {LNCS ARCoSS},
volume = {8312}
}
@inproceedings{MBouOHer13,
author = {M{\'e}lanie Boudard and
Olivier Hermant},
title = {Polarizing Double-Negation Translations},
booktitle = {LPAR},
year = {2013},
pages = {182-197},
editor = {Ken McMillan and
Aart Middeldorp and
Andre{\"i} Voronkov},
publisher = {Springer},
series = {LNCS ARCoSS},
volume = {8312}
}
@inproceedings{DDelDDolFGilPHalOHer13,
author = {David Delahaye and
Damien Doligez and
Fr{\'e}d{\'e}ric Gilbert and
Pierre Halmagrand and
Olivier Hermant},
title = {Zenon Modulo: When Achilles Outruns the Tortoise using
Deduction Modulo},
booktitle = {LPAR},
year = {2013},
pages = {274-290},
editor = {Ken McMillan and
Aart Middledorp and
Andre{\"i} Voronkov},
publisher = {Springer},
series = {LNCS ARCoSS},
volume = {8312}
}
@inproceedings{DDelDDolFGilPHalOHer13b,
author = {David Delahaye and
Damien Doligez and
Fr{\'e}d{\'e}ric Gilbert and
Pierre Halmagrand and
Olivier Hermant},
title = {Proof Certification in Zenon Modulo: When Achilles
Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps},
booktitle = {IWIL, 10th International Workshop on the Implementation of Logics},
year = {2013},
pages = {},
editor = {}
}
@inproceedings{GBurDDelDDolPHalOHer15,
author = {Guillaume Bury and
David Delahaye and
Damien Doligez and
Pierre Halmagrand and
Olivier Hermant},
title = {Automated Deduction in the {B} Set Theory using Typed Proof Search
and Deduction Modulo},
booktitle = {20th International Conferences on Logic for Programming, Artificial
Intelligence and Reasoning - Short Presentations, {LPAR} 2015, Suva,
Fiji, November 24--28, 2015.},
pages = {42--58},
year = {2015},
editor = {Ansgar Fehnker and
Annabelle McIver and
Geoff Sutcliffe and
Andrei Voronkov},
series = {EPiC Series in Computing},
volume = {35},
publisher = {EasyChair},
url = {http://www.easychair.org/publications/volume/LPAR-20},
}
@inproceedings{GGilOHer15,
author = {Ga{\"{e}}tan Gilbert and
Olivier Hermant},
title = {Normalisation by Completeness with Heyting Algebras},
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 20th
International Conference, {LPAR-20} 2015, Suva, Fiji, November 24-28,
2015, Proceedings},
pages = {469--482},
year = {2015},
editor = {Martin Davis and
Ansgar Fehnker and
Annabelle McIver and
Andrei Voronkov},
series = {Lecture Notes in Computer Science},
volume = {9450},
publisher = {Springer},
url = {http://dx.doi.org/10.1007/978-3-662-48899-7},
doi = {10.1007/978-3-662-48899-7},
isbn = {978-3-662-48898-0},
}