Reflexion, computation and logic
Réflexion, calculs et logiques
Résumé
The goal of my Ph.D. is to finds high level models in which self-modification can be expressed. What is readable and changeable is a data, and a program is executable. We propose an abstract machine where this duality is structurally emphasized. On one hand the program zone beholds registers which can be executed, and on the other hand data zone contains readable and changeable registers. Self-modification is enabled by passing a data register into program zone, or a program register into data zone. In this case, we give an abstraction of executions which only extracts information about self-modifications: execution is cut into paths without self-modification. For the logical part, we tried to find a Curry-Howard correspondence between a language with self-modifications and logical world. For that we built an extension of lambda-calculus with frozen terms, noted , that is, terms which cannot reduce. This terms are considered as data. Other terms are programs. We first prove that this language as expected properties like confluence. On the other hand, we found a type system where a subset of terms of this language can be expressed. Our type system is inspired by Linear Logic, without resources management. We prove that this system has good properties like subject reduction. We finally have extended the system with continuation and double negation. This extension can be expressed in a krivine style, using a machine inspired by krivine machine
Le but de cette thèse est de trouver des modèles de haut niveau dans lesquelles l'auto-modification s'exprime facilement. Une donnée est lisible et modifiable, alors qu'un programme est exécutable. On décrit une machine abstraite où cette dualité est structurellement mise en valeur. D'une part une zone de programmes contient tous les registres exécutables, et d'autre part une zone de données contient les registres lisibles et exécutables. L'auto-modification est permise par le passage d'un registre d'une zone à l'autre. Dans ce cadre, on donne une abstraction de l'exécution de la machine qui extrait seulement les informations d'auto-modification. Logiquement, on essaye de trouver une correspondance de Curry-Howard entre un langage avec auto-modification et un système logique. Dans ce but on construit une extension de lambda-calcul avec termes gelés, c'est à dire des termes qui ne peuvent se réduire. Ces termes sont alors considérés comme des données, et les autres sont les programmes. Notre langage a les propriétés usuelles du lambda-calcul (confluence). D'autre part, on donne un système de types dans lequel un sous ensemble des termes du langage peuvent s'exprimer. Ce système est inspiré de la Logique Linéaire, sans gestion des ressources. On prouve que ce système de types a de bonnes propriétés, comme celle de la réduction du sujet. Finalement, on étend le système avec les continuations et la double négation, dans un style à la Krivine
Origine : Version validée par le jury (STAR)
Loading...