Syntaxe et modèles d'une composition non-associative des programmes et des preuves

• Main Author: Munch-Maccagnoni, Guillaume
• Language: ENG
• Published: Université Paris-Diderot - Paris VII 2013
• Subjects: [INFO:INFO_LO] Computer Science/Logic in Computer Science; [INFO:INFO_LO] Informatique/Logique en informatique; [INFO:INFO_PL] Computer Science/Programming Languages; [INFO:INFO_PL] Informatique/Langage de programmation; Composition non-associative; Polarisation; Adjonctions; Modèle direct; Machine abstraite; Calcul de séquents; Contrôle délimité; CPS
• Online Access: http://tel.archives-ouvertes.fr/tel-00918642; http://tel.archives-ouvertes.fr/docs/00/91/86/42/PDF/these-screen-final.pdf

La thèse contribue à la compréhension de la nature, du rôle et des mécanismes de la polarisation dans les langages de programmation, en théorie de la preuve et dans les modèles catégoriels. La polarisation correspond à l'idée que la condition d'associativité de la composition peut être relâchée, comme on le montre à travers un résultat qui relie les duploïdes, notre modèle direct de la polarisation, aux adjonctions. En conséquence, la polarisation sous-tend de nombreux modèles du calcul, ce que l'on souligne encore en montrant comment les modèles par passage de continuation pour des opérateurs de contrôle délimité se décomposent en trois étapes fondamentales. Elle explique également des phénomènes de constructivité en théorie de la démonstration, ce que l'on illustre en donnant une interprétation selon le principe de la formule comme type à la polarisation en général et à une négation involutive en particulier. Notre approche est basée sur une représentation interactive des démonstrations et des programmes à base de termes (calcul L), qui met en évidence la structure des polarités. Celle-ci est basée sur la correspondance entre les machines abstraites et les calculs de séquents, et vise à synthétiser diverses directions : la modélisation du contrôle, de l'ordre d'évaluation et des effets dans les langages de programmation, la quête d'un lien entre la dualité catégorielle et les continuations, et l'approche interactive de la constructivité en théorie de la preuve. On introduit notre technique en supposant uniquement une connaissance élémentaire du λ-calcul simplement typé et de la réécriture.