Le calcul dans les topos relatifs et l’interprétation du langage W

Mémoire de Master 2 réalisé par M. Cadet sous ma direction. Dans ce mémoire, la traduction précise entre le langage interne d'un topos relatif T/X (où X est un objet de T) et le langage natif du topos T est explicitée. Dans une seconde partie, cet traduction est exploitée pour interpréter le langage W, qui est une variante ``à types dépendants'' du langage interne des topos.