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

This document was translated from L^AT_EX by H^EV^EA.