Theoretical studies

• Conception d'un langage de haut niveau de representation de preuves: Récurrence par filtrage de motifs; Unification en présence de types inductifs primitifs; Synthèse de lemmes d'inversion.
  Cristina Cornes , Thèse de Doctorat de l'Universitè de Paris 7. November, 1997
• A Theory of Specifications, Programs and Proofs.
  Nora Szasz , Ph.D. Thesis, Dept. of Computing Science, Chalmers University of Technology, Gothenburg, 1997.
• Extension of Martin-Löf's type theory with record types and subtyping.
  Gustavo Betarte, Alvaro Tasistro. Twenty Five Years of Constructive Type Theory, Oxford University Press, pp. 21 - 39, 1998.