Extending Implicit Computational Complexity and Abstract Machines to Languages with Control

Giulio Pellitta 1, 2
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
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 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.
Document type :
Theses
Complete list of metadatas

Cited literature [171 references]  Display  Hide  Download

https://hal.inria.fr/tel-01090624
Contributor : Giulio Pellitta <>
Submitted on : Wednesday, December 3, 2014 - 6:31:27 PM
Last modification on : Saturday, January 27, 2018 - 1:31:05 AM
Long-term archiving on : Monday, March 9, 2015 - 5:52:59 AM

File

Identifiers

  • HAL Id : tel-01090624, version 1

Collections

Citation

Giulio Pellitta. Extending Implicit Computational Complexity and Abstract Machines to Languages with Control. Programming Languages [cs.PL]. Università di Bologna, 2014. English. ⟨tel-01090624⟩

Share

Metrics

Record views

198

Files downloads

188