Nested Deduction in Logical Foundations for Computation
Deduction Imbriquée et Fondements Logiques du Calcul
Résumé
This thesis investigates the use of deep inference formalisms as basis for a computational interpretation of proof systems, following the two main approaches: proofs-as-programs and proof-search-as-computation. The first contribution is the development of a family of proof systems for intuitionistic logic in the calculus of structures and in nested sequents, for which internal normalisation procedures are given. One of these procedure is then interpreted in terms of computation, as a refinement of the Curry-Howard correspondence allowing to introduce a form of sharing and communication operators in a lambda-calculus with explicit substitution. On the side of proof-search, the notion of focused proof in linear logic is transferred from the sequent calculus into the calculus of structures, where it yields an incremental form of focusing, with a simple proof of completeness. Finally, another interpretation of proof-search is given through the encoding of reduction in a lambda-calculus with explicit substitution into the inference rules of a subsystem of intuitionistic logic in the calculus of structures.
Cette thèse s'intéresse à l'usage des formalismes d'inférence profonde comme fondement des interprétations calculatoires des systèmes de preuve, en suivant les deux approches principales: celle des preuves comme programmes et celle de la recherche de preuve comme calcul. La première contribution est le développement d'une famille de systèmes de preuve pour la logique intuitionniste dans le calcul des structures et dans les séquents imbriqués. pour lesquels des procédures de normalisation internes sont fournies. L'une de ces procédures est alors interprétée en termes calculatoires, comme un raffinement de la correspondance de Curry-Howard permettant d'introduire une forme de partage ainsi que des opérateurs de communication dans un lambda-calcul avec substitution explicite. Du coté de la recherche de preuve, la notion de preuve focalisée en logique linéaire est transférée du calcul des séquents au calcul des structures, où elle induit une forme incrémentale de focalisation, dotée d'une preuve de complétude très simple. Enfin, une autre interprétation de la recherche de preuve est donnée par l'encodage de la réduction d'un lambda-calcul avec substitution explicite dans les règles d'inférence d'un sous-système de la logique intuitionniste dans le calcul des structures.
Loading...