Textes d’informatiques

Sémantique catégorique du typage dépendant (transparents(.pdf), source(.tex))

Cet exposé a été donné dans le cadre du cours intitulé « Lambda-calculs et catégories » de Paul-André Melliès. Il se base sur l’article « Syntax and Semantics of Dependent Types(.pdf) » de Martin Hofmann. Je définis un lambda-calcul avec typage dépendant, suffisant pour pouvoir programmer la concaténation de listes avec un type tenant compte des longueurs des listes, puis j’explique comment définir des modèles catégoriques pour ce lambda-calcul.