Return to search

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

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.

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00918642
Date10 December 2013
CreatorsMunch-Maccagnoni, Guillaume
PublisherUniversité Paris-Diderot - Paris VII
Source SetsCCSD theses-EN-ligne, France
LanguageEnglish
Detected LanguageFrench
TypePhD thesis

Page generated in 0.0018 seconds