Extending Implicit Computational Complexity and Abstract Machines to Languages with Control
Extension de la Complexité Implicite et des Machines Abstraites aux Langues avec Contrôle
Résumé
The Curry-Howard isomorphism is the idea that proofs in natural deduction can be put in correspondence with lambda terms in such a way that this correspondence is preserved by normalization. The concept can be extended from Intuitionistic Logic to other systems, such as Linear Logic. One of the nice consequences of this isomorphism is that we can reason about functional programs with formal tools which are typical of proof systems: such analysis can also include quantitative qualities of programs, such as the number of steps it takes to terminate. Another is the possibility to describe the execution of these programs in terms of abstract machines.In 1990 Griffin proved that the correspondence can be extended to Classical Logic and control operators. That is, Classical Logic adds the possibility to manipulate continuations. In this thesis we see how the things we described above work in this larger context.
L'isomorphisme de Curry-Howard est l'idée que les preuves en déduction naturelle peuvent être mises en correspondance avec lambda-termes de telle manière que cette correspondance est préservée par la normalisation. Le concept peut être étendu à partir intuitionniste Logique à d'autres systèmes, tels que la logique linéaire. Une des belles conséquences de cet isomorphisme est que nous pouvons raisonner sur des programmes fonctionnels avec des outils formels qui sont typiques des systèmes de preuve: une telle analyse peut également inclure qualités quantitatives de programmes, tels que le nombre d'étapes nécessaires pour la terminaison. Un autre est la possibilité de décrire l'exécution de ces programmes en termes de machines abstraites.En 1990, Griffin a prouvé que la correspondance peut être étendue à des opérateurs logiques et de contrôle classiques. Ce est à dire, la logique classique ajoute la possibilité de manipuler des continuations. Dans cette thèse, nous voyons comment les choses que nous décrites ci-dessus travail dans ce contexte plus large.
Loading...