Olivier Hermant, Ph.D.
Cette page est obsolète. Visitez ma nouvelle page web à l'adresse suivante:
http://perso.isep.fr/ohermant/ si vous n'y êtes pas redirigés automatiquement dans 3 secondes.
This is an obsolete web page. Please visit my new webpage at the above adress, if you are not redirected within 3 seconds.
Esta p´gina es obsoleta. Ir a mi nueva pgina
Ici, vous pouvez trouver mon curriculum vitæ, mes articles et les transparents de mes exposés, un résumé de ma thèse de doctorat, et les documents la concernant, plus un programme de recherche étendu. Pour finir, quelques documents inédits et quelques liens.

Curriculum Vitæ

Mon CV, mis à jour Décembre 2007, avec la description de mes publications. Version anglaise sur la page en anglais:
  • au format [pdf]
  • au format [ps]
  • au format [ps.gz]
Haut CV Articles Thèse Divers

Articles et exposés

Dans des journaux

1. O. Hermant, Skolemization in various intuitionistic logics, Archive for Mathematical Logic, 2008 (to appear): ps et pdf bientôt, [bibtex]
2. O. Hermant et J. Lipton, Cut elimination in the Intuitionistic Theory of Types with Axioms and Rewriting Cuts, Constructively, dans: C. Benzmüller, C. E. Brown, J. Siekmann et R. Stateman, eds., Festschrift in Honor of Peter B. Andrews on his 70th Birthday, Studies in Logic and the Foundations of Mathematics, IfCoLog, 2008 (à paraître): ps et pdf bientôt, [bibtex]
3. O. Hermant et J. Lipton, A note on Completeness and cut elimination in the Intuitionistic Church's Theory of Types, Journal of Logic and Computation, 2008 (à para\ître): ps et pdf bientôt, [bibtex]

Dans des actes de conférence internationale

4. O. Hermant et J. Lipton, A constructive semantic approach to cut elimination in type theories with axioms, CSL'08, 2008 (à paraître): ps et pdf bientôt, [bibtex]
5. G. Dowek et O. Hermant, A simple proof that super consistency implies cut elimination, proceedings of RTA'07, LNCS 4533, pp. 93-106, 2007: [ps], [ps.gz], [pdf], [bibtex], [lien]
Les transparents: [ps], [ps.gz], [pdf]
6. R. Bonichon et O. Hermant, On constructive cut admissibility in deduction modulo, post-proceedings of TYPES'06, LNCS 4502, pp. 41-50, 2007: [ps], [ps.gz], [pdf], [bibtex], [lien]
7. R. Bonichon et O. Hermant, A semantic completeness proof for TaMeD, proceedings of LPAR'06, Phnom Penh, Cambodia, LNCS 4246, pp. 167-181, 2006: [ps], [ps.gz], [pdf], [bibtex], [lien]
Les transparents de la présentation (par Richard Bonichon): [ps], [ps.gz], [pdf]
8. O. Hermant, Semantic cut elimination in the Intuitionnistic Sequent Calculus, proceedings of TLCA'05, Nara, Japan, LNCS 3461, pp. 221-233, 2005: [ps], [ps.gz], [pdf], [bibtex], [lien]
Les transparents: [ps], [ps.gz], [pdf]

Dans des conférences internationales

9. O. Hermant, A Model-based cut elimination proof, 2nd St-Petersburg Days of Logic and Computability, St-Pétersbourg, 2003: [ps], [ps.gz], [pdf], [bibtex]
Les transparents: [ps], [ps.gz], [pdf]

Workshops

10. A linear logic modulo, 1st Workshop on Type theory, proof theory and rewriting, Paris (France), Juin 2007: [ps], [ps.gz], [pdf]
11. A semantical cut elimination in intuitionistic deduction modulo, TYPES'04, Jouy-en-Josas (France), Dec. 2004: [ps], [ps.gz], [pdf]
12. Compilation of rewrite rules, 2nd workshop on Coq + rewriting, Ecole polytechnique, Palaiseau (France), 2004: [ps], [ps.gz], [pdf]

Exposés et Séminaires

  • PPS, Paris (France), 18 Mars 2008: [ps], [ps.gz], [pdf]
  • LIP, ENS Lyon (France), 11 Mar. 2008: [ps], [ps.gz], [pdf]
  • Wesleyan University, Middletown, CT (Etats-Unis), Dec. 2007: [ps], [ps.gz], [pdf]
  • Politecnica de Madrid (Espagne), Nov. 2007: [ps], [ps.gz], [pdf]
  • Complutense de Madrid (Espagne), Sep. 2007: [ps], [ps.gz], [pdf] et la [vidéo]
  • Séminaire MeASI, CEA-CNRS-Ecole polytechnique, Jun. 2007: [ps], [ps.gz], [pdf]
  • Wesleyan University, Middletown, CT (Etats-Unis), Dec. 2006: [ps], [ps.gz], [pdf]
  • Créteil (France), invité, Oct. 2007: [ps], [ps.gz], [pdf]
  • Keio University, Tokyo (Japon), Jun.-Jui. 2006: exposé au tableau, un poster A1: [pdf]
  • Univ. Paris 11, LRI, Orsay (France), Mai 2006: [ps], [ps.gz], [pdf]
  • Univ. Paris 7, PPS, Paris (France), Jan. 2004: [ps], [ps.gz], [pdf]
  • Marktoberdorf (Allemagne), Aoû. 2003: [ps], [ps.gz], [pdf]
Haut CV Articles Thèse Divers

Thèse de doctorat

Le résumé de ma thèse et de sa soutenance.
Le manuscript de thèse: [ps], [ps.gz], [pdf], [pdf.gz], [bibtex]
Les transparents de la soutenance: [ps], [ps.gz], [pdf]
Le rapport de soutenance et les pré-rapports de soutenance sont protégés en lecture. Veuillez me demander l'autorisation pour y avoir accès. De même, demandez-mois l'autorisation si vous voulez lire mon programme de recherche détaillé.
Haut CV Articles Thèse Divers

Divers

Documents

Ici, quelques documents rédigés qui n'ont pas (ou pas encore) donné lieu à des articles:
  • Une logique linéaire modulo: [ps], [ps.gz], [pdf]
  • Compilation des règles de réécriture vers une machine virtuelle: [ps], [ps.gz], [pdf]
  • Completness of Cut-Free Sequent Calculus Modulo (2004, 28 pp.):[ps], [ps.gz], [pdf]. Extension du papier de Saint-Pétersbourg avec plusieures conditions, dont la logique d'ordre supérieure.
  • Mémoire de DEA italien (2002) intitulé "Déduction modulo et élimination des coupures: une approche syntaxique". J'y étudie les liens entre résolution modulo et calcul des séquents modulo sans coupure. Résumé en italien: [ps], [ps.gz], [pdf]

Liens

Les pages de mes co-auteurs: Richard Bonichon, Mitsu Okada, Gilles Dowek et Jim Lipton. Pour la déduction modulo, on pourra aussi consulter avec profit les pages de Thérèse Hardin, Claude Kirchner ou bien directement celles de Typical et Pareo. On pourra aussi aller sur cette dernière pour se renseigner sur le rho-calcul. Enfin, une page pour la logique nominale de Jamie Gabbay.
Haut CV Articles Thèse Divers