Pellitta, Giulio
(2014)
Extending Implicit Computational Complexity and Abstract Machines to Languages with Control, [Dissertation thesis], Alma Mater Studiorum Università di Bologna.
Dottorato di ricerca in
Informatica, 26 Ciclo. DOI 10.6092/unibo/amsdottorato/6558.
Documenti full-text disponibili:
Abstract
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 conseguences 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 possiblity 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 possiblity to manipulate continuations. In this thesis we see how the things we described above work in this larger context.
Abstract
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 conseguences 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 possiblity 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 possiblity to manipulate continuations. In this thesis we see how the things we described above work in this larger context.
Tipologia del documento
Tesi di dottorato
Autore
Pellitta, Giulio
Supervisore
Dottorato di ricerca
Scuola di dottorato
Scienze e ingegneria dell'informazione
Ciclo
26
Coordinatore
Settore disciplinare
Settore concorsuale
Parole chiave
Functional Programming, Linear Logic, Control operators, Lambda Calculus, Lambda-mu Calculus, Abstract Machines, Implicit Computational Complexity, Type systems
URN:NBN
DOI
10.6092/unibo/amsdottorato/6558
Data di discussione
19 Maggio 2014
URI
Altri metadati
Tipologia del documento
Tesi di dottorato
Autore
Pellitta, Giulio
Supervisore
Dottorato di ricerca
Scuola di dottorato
Scienze e ingegneria dell'informazione
Ciclo
26
Coordinatore
Settore disciplinare
Settore concorsuale
Parole chiave
Functional Programming, Linear Logic, Control operators, Lambda Calculus, Lambda-mu Calculus, Abstract Machines, Implicit Computational Complexity, Type systems
URN:NBN
DOI
10.6092/unibo/amsdottorato/6558
Data di discussione
19 Maggio 2014
URI
Statistica sui download
Gestione del documento: