IMPRO
Implicit Programming
| Coordinatore | ECOLE POLYTECHNIQUE FEDERALE DE LAUSANNE
Spiacenti, non ci sono informazioni su questo coordinatore. Contattare Fabio per maggiori infomrazioni, grazie. |
| Nazionalità Coordinatore | Switzerland [CH] |
| Totale costo | 1˙439˙240 € |
| EC contributo | 1˙439˙240 € |
| Programma | FP7-IDEAS-ERC
Specific programme: "Ideas" implementing the Seventh Framework Programme of the European Community for research, technological development and demonstration activities (2007 to 2013) |
| Code Call | ERC-2012-StG_20111012 |
| Funding Scheme | ERC-SG |
| Anno di inizio | 2012 |
| Periodo (anno-mese-giorno) | 2012-12-01 - 2017-11-30 |
Partecipanti
| # | ||||
|---|---|---|---|---|
| 1 |
ECOLE POLYTECHNIQUE FEDERALE DE LAUSANNE
Organization address
address: BATIMENT CE 3316 STATION 1 contact info |
CH (LAUSANNE) | hostInstitution | 1˙439˙240.00 |
| 2 |
ECOLE POLYTECHNIQUE FEDERALE DE LAUSANNE
Organization address
address: BATIMENT CE 3316 STATION 1 contact info |
CH (LAUSANNE) | hostInstitution | 1˙439˙240.00 |
Mappa
Word cloud
Esplora la "nuvola delle parole (Word Cloud) per avere un'idea di massima del progetto.
Obiettivo del progetto (Objective)
'I propose implicit programming, a paradigm for developing reliable software using new programming language specification constructs and tools, supported through the new notion of software synthesis procedures. The paradigm will enable developers to use specifications as executable programming language constructs and will automate some of the program construction tasks to the point where they become feasible for the end users. Implicit programming will increase developer productivity by enabling developers to focus on the desired software functionality instead of worrying about low-level implementation details. Implicit programming will also improve software reliability, because the presence of specifications will make programs easier to analyze.
From the algorithmic perspective, I propose a new agenda for research in algorithms for decidable logical theories. An input to such an algorithm is a logical formula (or a boolean-valued programming language expressions). Whereas a decision procedure for satisfiability merely checks whether there exists a satisfying assignment for the formula, we propose to develop synthesis procedures. A synthesis procedure views the input as a relation between inputs and outputs, and produces a function from input variables to output variables. In other words, it transforms a specification into a computable function. We will design synthesis procedures for important classes of formulas motivated by useful programming language fragments. We will use synthesis procedures as a compilation mechanism for declarative programming language constructs, ensuring correctness by construction. To develop practical synthesis procedures we will combine insights from decision procedure research (including the results on SMT solvers), with the research on compiler construction, program analysis, and program transformation. The experience from the rich model toolkit initiative (http://RichModels.org) will help us address these goals.'