SIMPL
Specification and Implementation of Pattern Languages
| Coordinatore | THE UNIVERSITY COURT OF THE UNIVERSITY OF ST ANDREWS
Organization address
address: NORTH STREET 66 COLLEGE GATE contact info |
| Nazionalità Coordinatore | United Kingdom [UK] |
| Totale costo | 173˙903 € |
| EC contributo | 173˙903 € |
| Programma | FP7-PEOPLE
Specific programme "People" implementing the Seventh Framework Programme of the European Community for research, technological development and demonstration activities (2007 to 2013) |
| Code Call | FP7-PEOPLE-2009-IEF |
| Funding Scheme | MC-IEF |
| Anno di inizio | 2010 |
| Periodo (anno-mese-giorno) | 2010-04-01 - 2012-03-31 |
Partecipanti
| # | ||||
|---|---|---|---|---|
| 1 |
THE UNIVERSITY COURT OF THE UNIVERSITY OF ST ANDREWS
Organization address
address: NORTH STREET 66 COLLEGE GATE contact info |
UK (ST ANDREWS FIFE) | coordinator | 173˙903.20 |
Mappa
Word cloud
Esplora la "nuvola delle parole (Word Cloud) per avere un'idea di massima del progetto.
Obiettivo del progetto (Objective)
'The proposal is aimed at helping to provide robust and transparent data infrastructure for the future Internet (which is a part of the European Commission ICT Challenge 1: Pervasive and Trustworthy Network and Service Infrastructures). The primary object of research is data, in contrast with computation. Therefore we will be interested mainly in kinds of formal data certification rather than in certified interpreters, etc. This however does not exclude possibilities for a crossroad research where these two paradigms overlap. Research objectives: 1) Theoretical representation of extended, or, practical, regular expressions in constructive dependent type theory. (We will overcome redundant assumptions regarding equality of languages that lay in the foundation of today's simply typed theories of practical regular expressions.) 2) A Coq library for regular languages and automata that includes features not present in available related libraries, such as extended regular expressions and partial derivatives of regular expressions; and a Coq library for pattern languages that provides full support for backreferences. 3) A formally certified compiler of patterns into automata; a formally certified grep-like pattern parser. 4) A formally certified UTF-8 encoder/decoder. 5) A formally certified data description language for describing binary data format specifications with a possibility to prove meta-properties of data specifications, such as completeness or consistency; in other words, a language for production of formally certified specifications of data formats. Main research questions: 1) What is the efficiency of the derivative approach in computation of context-sensitive features or extended regular expressions? 2) How can one define partial derivatives of regular expressions with backreferences? 3) What is the dependent type of partial derivatives of regular expressions with backreferences?'