PLATFORM

PRACTICAL LIGHT TYPES FOR RESOURCE CONSUMPTION

 Partecipanti

Mappa

 Word cloud

Esplora la "nuvola delle parole (Word Cloud) per avere un'idea di massima del progetto.

 Obiettivo del progetto (Objective)

'Eliminating errors early in the software-design life cycle is crucial to reduce the tremendous societal cost represented by defective software. Modern programming languages offer a variety of techniques for ensuring, at design time, the correctness of software systems with respect to the desired behaviors. However, these techniques do not consider usually the software aspects related to programs resource consumption, in terms of execution time, memory space, energy consumption, etc. So, new contributions and novel challenging ideas are needed. The present project aims at filling this gap achieving three main goals: 1-Showing that a concrete methodology combining the resource management facilities offered by light linear type systems and by the ideas of implicit computational complexity, with the features usually offered by practical programming languages provides extremely accurate information about the behavior of concrete programs and their resource consumption. 2-Developing a practical programming language integrating the resulting methodology in the form of a precise type system where types contain information, in the form of dependent types, about the resources needed by programs during their execution and where type checking a program will naturally corresponds to exhibit a certification of its resource consumption. 3-Demonstrating the successfulness of the language by implementing concrete resource-sensible applications. This will be done by targeting concrete examples taken from compiler correctness and component-based programming. In particular, in the latter, the modularity offered by the use of type systems will be useful to express resource consumption constraints per component, and to combine them over compositions of components. The broader interest of this proposal lies in the opportunities it will supply to improve the software quality by eliminating errors, usually difficult to fix, related to programs resource consumption.'

Introduzione (Teaser)

An EU team aimed to develop software error-removal tools specifically for differential privacy uses. The developments address resource consumption and privacy budget, with the prototype algorithm showing improved performance.

Descrizione progetto (Article)

The social costs of defective software can be prevented through removing design errors, and modern programming languages include error-removal tools. Generally, however, such techniques do not consider resource consumption.

With EU funding, the PLATFORM (Practical light types for resource consumption) project aimed to develop software error-removal tools addressing resource consumption. The efforts were focused on differential privacy applications. The two-partner project ran for three years from mid-2011.

First-year work involved study of a type-based framework, useful in inferring an application's execution time consumption. The benefit was the ability to analyse different resolution models, making the technique widely applicable and modular.

During the following year, the researchers designed a methodology, using a domain-specific programming language, for automatically determining the privacy budget used by an application.

The final year's work focused on applying the previously developed techniques to both resource consumption and differential privacy. Researchers extended the theory and practice of the latter, including an economic model describing how to set the relevant defining parameters. The resulting algorithm showed good performance. The project's novel verification technique also proved useful.

PLATFORM achieved a new theory applicable to uniformly describing several resource analyses. An additional result was researcher training and development.