Computing with relations, functions, and bindings

Calculer avec des relations, des fonctions et des lieurs Cette thèse s'inscrit dans la longue tradition de l'étude des relations entre logique mathématique et calcul et plus spécifiquement de la programmation déclarative. Le document est divisé en deux contributions principales. Chacune d'entre-elles utilise des résultats récents de la théorie de la démonstration pour développer de techniques novatrices utilisant déduction logique et fonctions pour effectuer des calculs. La première contribution de ce travail consiste en la description et la formalisation d'une nouvelle technique utilisant le mécanisme de la focalisation (un moyen de guider la recherche de preuve) pour distinguer les calculs fonctionnels qui se dissimulent dans les preuves déductives. À cet effet nous formulons un calcul des séquents focalisé pour l'arithmétique de Heyting où points-fixes et égalité sont définis comme des connecteurs logiques et nous décrivons une méthode pour toujours placer les prédicats singletons dans des phases négatives de la preuve, les identifiant ainsi avec un calcul fonctionnel. Cette technique n'étend en aucune façon la logique sous-jacente: ni opérateur de choix, ni règles de réécritures ne sont nécessaires. Notre logique reste donc purement relationnelle même lorsqu'elle calcule des fonctions. La seconde contribution de cette thèse et le design d'un nouveau langage de programmation fonctionnel: MLTS. De nouveau, nous utilisons des travaux théoriques récents en logique: la sémantique de mlts est ainsi une théorie au sein de la logique G, la logique de raisonnement de l'assistant de preuve Abella. La logique G utilise un opérateur spécifique: Nabla, qui est un quantificateur sur des noms "frais" et autorise un traitement naturel des pruves manipulant des objets pouvant contenir des lieurs. Ce traitement s'appuie sur la gestion naturelle des lieurs fournie par le calcul des séquents. La syntaxe de MLTS est basée sur celle du langage de programmation OCaml mais fournit des constructions additionnelles permettant aux lieurs présents dans les termes de se déplacer au niveau du programme. De plus, toutes les opérations sur la syntaxe respectent l'alpha et la béta conversion. Ces deux aspects forment l'approche syntaxique des lieurs appelée lambda-tree syntax. Un prototype d'implémentation du langage est fourni, permettant à chacun d'expérimenter facilement en ligne (url{https://trymlts.github.io}).