Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 theses
Participation of G. Huet
to doctoral thesis committees
1974
Roger Dallard.
Présentation d’un programme de démonstration de théorèmes d’arithmétique.
Thèse de Doctorat de 3ème cycle.
U. Paris 6.
24-4-74
Examiner
1975
Bernard Luya.
Un système complet de déduction naturelle.
Thèse de Doctorat de 3ème cycle,
U. Paris 7.
21-1-75
Advisor
A. Hertz.
Programme de démonstration de théorèmes formulables en logique des prédicats
du premier ordre avec égalité.
Thèse de Doctorat de 3ème cycle,
U. Paris 6.
2-12-75
Examiner
1976
Jean-Louis Laurière.
Un langage et un programme pour énoncer et résoudre des problèmes combinatoires.
Thèse de Doctorat ès Sciences,
U. Paris 6.
21-5-76
Reviewer
1977
Guy Cousineau.
Les arbres à feuilles indicées : un cadre algébrique pour l’étude des
structures de contrôle.
Thèse de Doctorat ès Sciences
U. Paris 7
13-5-77
Examiner
Hubert Marchand.
Logique typée du premier ordre et cohérence sémantique des bases de
données.
Thèse de Doctorat de 3ème cycle,
U. Paris 6.
31-5-77
Examiner
Frédéric Boussinot.
La notion d’appel de procédure en EXEL.
Thèse de Doctorat de 3ème cycle,
U. Paris 7.
25-11-77
Examiner
Patrick Greussay.
Contributions à la définition interprétative et a l’implémentation des
lambda-langages.
Thèse de Doctorat ès Sciences,
U. Paris 7
11-77
Reviewer
1978
Jean-Jacques Lévy.
Réductions correctes et optimales dans le lambda-calcul.
Thèse de Doctorat ès Sciences,
U. Paris 7
17-1-78
Examiner
1979
Laurent Kott.
Des substitutions dans les systêmes d’equations algèbriques sur le magma.
Application aux transformations de programmes et à leur correction.
Thèse de Doctorat ès Sciences,
U. Paris 7
19-6-79
Examiner
1980
Jean-Marie Hullot.
Compilation de formes canoniques dans les théories équationnelles.
Thèse de Doctorat de 3ème cycle,
U. Paris 11
14-11-80
Advisor
1981
Daniel Goossens.
La meta-évaluation au service de la compréhension automatique de programmes.
Thèse de Doctorat de 3ème cycle,
U. Paris 7.
?-1-81
Examiner
Jean-Pierre Pécuchet.
Equations avec constantes et algorithme de Makanin.
Thèse de Doctorat de 3ème cycle,
U. de Rouen
21-12-81
Examiner
1982
Laurent Fribourg.
Démonstration automatique: réfutation par superposition de clauses
équationnelles.
Thèse de Doctorat de 3ème cycle,
U. Paris 7.
27-9-82
Examiner
1983
Philippe Le Chenadec.
Formes canoniques dans les algèbres finiment présentées.
Thèse de Doctorat de 3ème cycle,
U. Paris 11.
21-6-83.
Advisor
François Fages
Formes canoniques dans les algèbres booléennes et applications
à la démonstration automatique en logique de premier ordre.
Thèse de Doctorat de 3ème cycle,
U. Paris 7.
22-6-83
Advisor
Pierre-Louis Curien.
Combinateurs catégoriques, algorithmes séquentiels et programmation
applicative.
Thèse de Doctorat ès Sciences,
U. Paris 7.
2-12-83
Examiner
Laurence Puel.
Preuves dans l’algèbre terminale. Algorithmes de complétion.
Thèse de Doctorat de 3ème cycle,
U. Paris 7.
19-12-83
Examiner
1984
Daniel Singer.
Contributions à l’expression logique des mécanismes d’apprentissage.
Thèse de Doctorat de 3ème cycle,
U. Paris 6.
14-2-84.
Examiner
Michel Van Caneghem.
L’anatomie de PROLOG II.
Thèse de Doctorat ès Sciences,
U. d’Aix-Marseille II
24-10-84
Examiner
1985
Thierry Coquand.
Une théorie des Constructions.
Thèse de Doctorat de 3ème cycle,
U. Paris 7.
31-1-85.
Advisor
Claude Kirchner.
Méthodes et outils de conception systématique d’algorithmes d’unification
dans les théories équationnelles.
Thèse de Doctorat ès Sciences,
U. de Nancy 1
21-6-85
Reviewer
Hélène Kirchner.
Preuves par complétion dans les variétés d’algèbres.
Thèse de Doctorat ès Sciences,
U. de Nancy 1
21-6-85
Examiner
Jean-Jacques Lacrampe.
Etude, extension et implémentation de Manens : un langage applicatif pour la
manipulation des ensembles dans le cadre de la théorie des algorithmes.
Thèse de Doctorat de 3ème cycle,
U. d’Orleans
12-7-85
Examiner
1987
Habib Abdulrab.
Résolution d’équations sur les mots : étude et implémentation LISP
de l’algorithme de Makanin.
Thèse de Doctorat ès Sciences,
U. de Rouen
20-3-87
President of jury
Thérèse Hardin-Accart.
Résultats de Confluence pour les Règles Fortes de la Logique Combinatoire
Catégorique et Liens avec les Lambda-Calculs.
Thèse de Doctorat d’Informatique,
U. Paris 7.
27-10-87
Examiner
Pierre Weis.
Le système SAM : Metacompilation très efficace à l’aide d’opérateurs
sémantiques.
Thèse de Doctorat d’Informatique,
U. Paris 7.
16-11-87
Reviewer
1988
Yves Lafont.
Logiques, Catégories & Machines. Implantation de Langages de Programmation
guidée par la Logique Catégorique.
Thèse de Doctorat d’Informatique,
U. Paris 7.
7-1-88
Examiner
Alain Laville.
Evaluation Paresseuse des Filtrages avec Priorité. Application au Langage ML.
Thèse de Doctorat d’Informatique,
U. Paris 7.
17-2-88
Advisor
Hubert Comon.
Unification et disunification. Théorie et applications.
Thèse de Doctorat d’Informatique,
Institut National Polytechnique de Grenoble.
18-3-88
Examiner
Pierre Réty.
Méthodes d’unification par surréduction.
Thèse de Doctorat d’Informatique,
U. Nancy 1.
22-3-88
Examiner
Gérard Senizergues.
Sur la description des langages algébriques déterministes par des systèmes
de réécriture confluents.
Thèse de Doctorat d’Etat,
Mai 88.
Examiner
David Wolfram.
Foundations for Higher-Order Languages.
Trinity College Fellow, Cambridge University.
8-88
Reviewer
Thomas Ehrhard.
Une sémantique Catégorique des Types Dépendants. Application au Calcul des
Constructions.
Thèse de Doctorat d’Informatique,
U. Paris 7.
26-9-88
Reviewer
1989
Christine Paulin-Mohring.
Extraction de programmes dans le Calcul des Constructions.
Thèse de Doctorat d’Informatique,
U. Paris 7.
27-1-89
Advisor
Yves Auffray.
Résolution modale et logique des chemins.
Thèse de Doctorat d’Informatique,
U. Caen.
15-3-89
President of jury
Conal Elliott.
Extensions and Applications of Higher-order Unification.
Ph. D. Thesis,
U. Carnegie-Mellon, Pittsburgh.
1-6-89
Examiner
Pascal Weil.
Problèmes de composition et de décomposition en théorie des langages.
Memoire d’habilitation, Informatique,
U. Paris 6.
27-11-89
Examiner
1990
Annie Forêt.
Algèbres des logiques modales et intuitionistes:
procédures de décision et formes canoniques.
Thèse de Doctorat d’Informatique,
U. Paris 7.
17-1-90
Advisor
Paul Gloess.
Contribution à l’Optimisation de Mécanismes de Raisonnement dans des
Structures Spécialiséees de Représentation des Connaissances.
Thèse de Doctorat d’Etat,
Université de Technologie de Compiègne.
22-1-90
Advisor
Didier Rémy.
Algèbres touffues. Application au typage polymorphe des objets enregistrements
dans les langages fonctionnels.
Thèse de Doctorat d’Informatique,
U. Paris 7.
19-2-90
Advisor
Alexandre Boudet.
Unification dans les mélanges de théories équationnelles.
Thèse de Doctorat d’Informatique,
U. Paris XI.
21-2-90
Examiner
Hassan Ait Kaci.
Life.
Mémoire d’habilitation, Informatique,
U. Paris 7.
9-3-90
Examiner
El-Hassan Bezzazi.
Types de données et récurrence bien fondée dans un système de programmation
par preuves.
Doctorat d’Informatique,
Université des Sciences et Techniques de Lille Flandre Artois
4-7-90
Reviewer
Francis Dupont.
Langages fonctionnels et parallélisme. Une réalisation pour le langage
CAML.
Thèse d’informatique,
École Polytechnique.
5-7-90
Examiner
David Pym.
Proofs, search and computation in general logic.
PhD thesis,
U. of Edinburgh.
12-10-90
External Examiner
Philippe Besnard.
Approche logique des systèmes d’inférence non-monotones en intelligence
artificielle.
Mémoire d’habilitation, Informatique,
U. Rennes 1.
11-12-90
Examiner
François Rouaix
ALCOOL-90. Typage de la surcharge dans un langage fonctionnel.
Thèse d’informatique,
U. Paris 7.
20-12-90
Examiner
1991
Philippe de Groote.
Définition et propriétés d’un metacalcul de représentation de theories.
Thèse de Doctorat en Sciences Appliquées,
U. Catholique de Louvain.
29-1-91
Examiner
Loic Colson.
Représentation intentionnelle d’algorithmes dans les systèmes fonctionnels :
une étude de cas.
Thèse d’informatique,
U. Paris 7.
30-1-91
Advisor
Yves Bertot.
Une automatisation du calcul des résidus en sémantique naturelle.
Thèse d’informatique,
U. Nice.
6-6-91
Examiner
Pierre Crégut.
Machines à environnement pour la réduction symbolique et l’évaluation
partielle.
Thèse d’informatique,
U. Paris 7.
26-6-91
Examiner
Olivier Coudert.
SIAM : Une boîte à outils pour la preuve formelle de systèmes séquentiels.
Thèse d’informatique,
École Nationale Supérieure des Telecommunications.
10-10-91
Examiner
Emmanuel Chailloux.
Compilation des langages fonctionnels : CeML un traducteur de ML vers C.
Thèse d’informatique,
U. Paris 7.
19-11-91
Examiner
Jean Yves Marion.
Extension du systême T de Godel dans les domaines finis.
Thèse d’informatique,
U. Paris 7.
3-12-91
Examiner
Gilles Dowek.
Démonstration automatique dans le Calcul des Constructions.
Thèse d’informatique,
U. Paris 7.
16-12-91
Advisor
Thérèse Hardin.
Langages pour la substitution explicite et lambda-calculs.
Habilitation,
U. Paris 7.
16-12-91
Reviewer
1992
Alain Deutsch.
Modèles opérationnels de langages de programmation et représentations de
relations sur des langages rationnels avec application à la détermination
statique de propriétés de partages dynamiques de données.
Thèse d’informatique,
U. Paris 6
1-4-92
Examiner
Hubert Comon.
Résolution de Contraintes dans des Algèbres de Termes.
Habilitation,
U. Paris 11
3-4-92
Examiner
Evelyne Contejean.
Eléments pour la décidabilité de l’unification modulo la distributivité.
Thèse d’informatique,
U. Paris 11
3-4-92
President of jury
François Fages
Aspects sémantiques et algorithmiques de la déduction automatique.
Habilitation,
U. Paris 7
26-5-92
President of jury
Xavier Leroy.
Typage polymorphe d’un langage algorithmique
Thèse d’informatique,
U. Paris 7.
12-6-92
Advisor
Pascal Manoury.
Des preuves de totalité de fonctions comme synthèse de programmes.
Thèse d’informatique,
U. Paris 7.
4-12-92
President of jury
Marianne Simonot.
Des preuves de totalité de fonctions comme synthèse de programmes.
Thèse d’informatique,
U. Paris 7.
4-12-92
President of jury
1993
Ascander Suarez.
Une Implémentation de ML en ML.
Thèse d’informatique,
U. Paris 7.
25-1-93
Examiner
Thomas Ehrhard.
Stabilité Forte et Séquentialité.
Habilitation,
U. Paris 7
26-1-93
Examiner
Leen Helmink.
Tools for proofs and programs.
Promotion,
U. of Amsterdam
19-3-93
Reviewer
Jean Goubault.
Démonstration automatique en logique classique : complexité et méthodes.
Thèse d’informatique,
École Polytechnique
17-9-93
President of jury
Alain Coste.
Un systême pour la validation des développements de programmes :
Définition formelle et réalisation.
Thèse d’informatique,
U. Toulouse
29-9-93
Reviewer
Claude Marché.
Réécriture modulo une théorie présentée par un systême convergent et
décidabilité des problèmes du mot dans certaines classes de théories
équationnelles.
Thèse d’informatique,
U. Paris XI
1-10-93
President of jury
Delia Kesner.
Le définition de fonctions par cas à l’aide de motifs dans les langages applicatifs.
Thèse d’informatique,
U. Paris XI
17-12-93
President of jury
1994
Bruno Monsuez.
Typage par Interprétation Abstraite.
Thèse d’informatique,
École Polytechnique
8-2-94
President of jury
Christophe Raffali.
L’arithmétique fonctionnelle du second-ordre avec points fixes.
Thèse de mathématiques,
U. Paris VII
9-2-94
Examiner
Adel Bouhoula.
Preuves Automatiques par Induction dans les Théories Equationnelles.
Thèse d’informatique,
U. Nancy 1
13-3-94
President of jury
Joseph Rouyer.
Développements d’algorithmes dans le calcul des Constructions
Thèse d’informatique,
Institut National Polytechnique de Lorraine
14-3-94
President of jury
Benjamin Werner.
Une théorie des constructions inductives.
Thèse d’informatique,
U. Paris VII
2-5-94
Examiner
Erik Poll.
A Programming Language Based on Type Theory.
Promotion,
U. Eindhoven
20-9-94
Examiner
Valérie Menissier-Morain.
Arithmétique Exacte.
Thèse d’informatique,
U. Paris VII
8-12-94
Advisor
1995
Hugo Herbelin.
Séquents qu’on calcule.
Thèse d’informatique,
U. Paris VII
23-1-95
President of jury
Catherine Parent.
Synthèse de preuves de programmes dans le calcul des constructions inductives.
Thèse d’informatique,
ENS Lyon
24-1-95
Examiner
Jean Jourdan.
Concurrence et Coopération de Modèles Multiples dans les Systèmes de Contraintes.
Thèse d’informatique,
U. Paris VII
14-2-95
Examiner
Jan Springintveld.
Algorithms for Type Theory.
Doctorat,
U. Utrecht
12-5-95
Examiner
Yves Lafont.
Approches géométriques du calcul.
Habilitation,
U. de Marseille-Luminy
3-10-95
Examiner
Delphine Terrasse.
Vers un environnement de développement de preuves en Sémantique Naturelle.
Thèse d’informatique,
École Nationale des Ponts et Chaussées
31-10-95
President of jury
1996
Pierre Valarcher.
Intentionalité, Extensionalité et Récursion Primitive.
Thèse d’informatique,
U. Paris VII
24-1-96
President of jury
Tristan Crolard.
Extension de l’isomorphisme de Curry-Howard au traitement des exceptions.
Thèse d’informatique,
U. Paris VII
3-12-96
President of jury
Christine Paulin-Mohring.
Définitions Inductives en Théorie des Types d’Ordre Supérieur.
Habilitation,
U. Lyon I
13-12-96
President of jury
1997
Samuel Boutin.
Réflexions sur les quotients.
Thèse d’informatique,
U. Paris VII
30-4-97
Advisor
Jean Goubault-Larrecq.
Logique, complexité, démonstration automatique et thèmes connexes.
Habilitation,
U. Paris Dauphine
27-6-97
Reviewer and President of jury
César Muñoz Hurtado.
Un calcul de substitutions pour la représentation de preuves partielles
en théorie des types.
Thèse d’informatique,
U. Paris VII
4-11-97
Advisor
Cristina Cornes.
Conception d’un langage de haut niveau de représentation de preuves.
Thèse d’informatique,
U. Paris VII
14-11-97
Advisor
1998
Adel Bouhoula.
Mécanisation du raisonnement par récurrence.
Habilitation,
U. Nancy 1
11-3-98
President of jury
Roberto di Cosmo.
Réécriture avec axiomes extensionels et isomorphismes de types.
Habilitation,
U. Paris VII
29-4-98
Examiner
1999
Loic Colson.
Les systèmes fonctionnels : problèmes pratiques et théoriques.
Habilitation,
U. d’Auvergne Clermont-Ferrand I
26-1-99
Examiner
Georges Mounier.
Un lambda calcul intuitionniste avec exceptions.
Thèse d’informatique,
U. de Savoie
19-2-99
Reviewer and President of jury
Amokrane Saibi.
Outils Génériques de Modélisation et de Démonstration pour la Formalisation
des Mathématiques en Théorie des Types.
Application à la Théorie des Catégories.
Thèse d’informatique,
U. Paris 6
19-3-99
Advisor
Gilles Dowek.
La part du calcul.
Habilitation,
U. Paris 7
4-6-99
Examiner
David Nowak.
Spécification et preuve de systèmes réactifs.
Thèse d’informatique,
U. Rennes 1
1-10-99
Examiner
Bruno Barras.
Auto-validation d’un système de preuves avec familles inductives.
Thèse d’informatique,
U. Paris VII
17-11-99
Advisor
2001
Samuel Lacas.
Extensionnalité, syntaxe et prédicats de vérité.
Thèse d’informatique,
U. Paris VII
8-6-01
President of jury
Sylvain Pogodalla.
Réseaux de preuve et génération pour les grammaires de types logiques.
Thèse d’informatique,
Institut Polytechnique de Lorraine
29-9-01
Reviewer
2002
Christian Retoré.
Logique linéaire et syntaxe des langues.
Habilitation,
Université de Nantes
4-1-02
Reviewer
Jean-François Monin
Contribution aux méthodes formelles pour le logiciel.
Habilitation,
Université Paris-Sud
4-4-02
President of jury
2003
Virgile Prevosto.
Conception et implantation du langage FOC
pour le développement de logiciels certifiés.
Thèse d’informatique,
Université Paris 6,
15-9-03
Examiner
Guy Perrier.
Les grammaires d’interaction.
Habilitation,
Université Nancy 2,
12-11-03
Reviewer
2004
Solange Coupet.
Des preuves et des programmes.
Habilitation,
Université de Provence,
10-09-04
Reviewer
Claire Gardent.
Inférence et traitement automatique des langues.
Habilitation,
Université de Nancy 1,
21-09-04
Reviewer
2006
Benoît Sagot.
Analyse automatique du français : lexiques, formalismes, analyseurs.
Thèse d’informatique,
Université Paris 7,
7-4-06
Reviewer
Patrick Thévenin.
Vers un assistant à la preuve en langue naturelle.
Thèse d’informatique,
Université de Savoie (Chambéry),
5-12-06
Examiner
2007
Markus Forsberg.
Three Tools for Language Processing:
BNF Convertor, Functional Morphology, and Extract.
Doctor of Engineering Thesis,
Chalmers University, Göteborg,
25-09-07
Faculty Opponent
2008
Benjamin Werner.
Faire simple pour pouvoir faire compliqué. Contributions à une
Théorie des Types pratique.
Habilitation,
Université Paris-Sud,
18-04-08
Examiner
Pierre-Yves Strub.
Building decision procedures in the Calculus of Inductive Constructions.
Thèse d’informatique,
Ecole Polytechnique,
02-07-08
President