Abstract FR:

Les problemes de decision sont au cur des concepts de la calculabilite, a l'intersection de la mathematique constructive, de la logique formelle, et de l'informatique. En effet, les tentatives pour l'elaboration de methodes qui repondent effectivement a un probleme de decision sont a l'origine du calcul et de la machine. C'est le cas du calcul lambda type utilise en informatique pour developper des machines virtuelles pour les langages de programmation. Cette these presente un probleme de decision pour la theorie des categories dont le langage presente deux formes d'expressions : des objets et des fleches entre objets. Comme en algebre, l'egalite est utilisee de facon a exprimer les proprietes de la structure qui determinent des categories plus particulieres. En tant que theorie egalitaire, c'est naturellement que se pose le probleme de decision des egalites. Or ce probleme n'admet pas de solution generale. Dans ce contexte, nous nous interesserons plus precisement aux categories cartesiennes fermees qui presentent par leur structure des interets tant pour la mathematique que pour la logique et pour l'informatique, et donc pour la calculabilite. Nous montrons en introduisant une nouvelle forme de normalisation adaptee que la theorie des categories cartesiennes fermees admet une methode effective pour repondre au probleme de decision precedent. Les proprietes abordees font de cette theorie un support a l'etablissement d'une machine virtuelle.