Théories symétriques monoïdales closes, applications au lambda-calcul et aux bigraphes

• Main Author: Pardon, Aurélien
• Other Authors: Lyon, École normale supérieure
• Language: fr
• Published: 2011
• Subjects: Catégories symétriques monoïdales closes; Théories de Lawvere; Réseaux de preuves; Lambda-calcul; Lambda-graphes; Bigraphes; Symmetric monoidal closed categories; Lawvere theories; Proof nets; Lambda-calculus; Lambda-graphs; Bigraphs
• Online Access: http://www.theses.fr/2011ENSL0622

En se fondant sur les travaux de Trimble et al., puis Hughes, on donne une notion de théorie symétrique monoïdale close (smc) et une construction explicite de la catégorie smc engendrée, formant ainsi une adjonction entre théories et catégories. On étudie les exemples du lambda-calcul pur linéaire, du lambda-calcul pur standard, puis des bigraphes de Milner. À chaque fois on donne une théorie smc et on compare la catégorie smc engendrée avec la présentation standard. Entre autres, dans les trois cas, on montre une équivalence entre les deux sur les termes clos. === From the work of Trimble et al. and Hughes, we define a notion of symmetric monoidal closed (smc) theory and give an explicit construction of the smc category generated by it. This construction yields a monadic adjunction between smc theories and smc categories. We study in our algebraic framework different models of programming languages: the linear λ-calculus, the pure λ-calculus and Milner's bigraphs. For each model, we give a smc theory and compare the generated smc category with the standard presentation. We show that, in each case, there is an equivalence on closed terms.