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
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
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,
Ecole 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.
Memoire 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,
Ecole Nationale Supérieure des Telecommunications.
10-10-91
Examiner
Emmanuel Chailloux
Compilatiion 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,
Ecole 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,
Ecole 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
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éometriques 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,
Ecole 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éfinition 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