Abstract FR:

Dans la théorie de la démonstration, la logique intuitionniste (LI) de brouwer et la logique linéaire (LL) de Girard définissent des preuves constructives (ou calculables) des formules mathématiques. Grâce à l'isomorphisme entre l'ensemble des preuves intuitionnistes et l'ensemble des lambda-termes types (curry-howard) et grâce à l'isomorphisme entre le lambda-calcul (non type) et l'ensemble des fonctions calculables par machine de Turing (Turing, Kleene), LI fait du lambda-calcul un modèle de langage de programmation par preuve. Le contenu du chapitre 4 contribue à faire jouer à ll un rôle analogue. Le fragment de LL considéré est le fragment multiplicatif et exponentiel avec les polarités de Danos et Regnier. L'ensemble des preuves est une traduction du lambda-calcul. Les preuves sont représentées par des structures de preuve sans concept de boites; la construction d'un espace cohérent modèle du lambda calcul (ch. 0) et de l'ensemble des réseaux de preuve fournit cette nouvelle définition en termes de graphes (ch. 1). Les structures de preuve (sans coupures) sont classifiées (ch. 3). En particulier les réseaux de preuve sans coupures sont les structures de preuve qui vérifient un critère de correction analogue à celui de Girard pour le fragment multiplicatif de LL. Ils correspondent aux lambda-termes normaux (ch. 4) et aux types principaux (ch. 5)