SIMPL

Specification and Implementation of Pattern Languages

Coordinatore	THE UNIVERSITY COURT OF THE UNIVERSITY OF ST ANDREWS    more  Organization address address: NORTH STREET 66 COLLEGE GATE city: ST ANDREWS FIFE postcode: KY16 9AJ contact info Titolo: Ms. Nome: Trish Cognome: Starrs Email: send email Telefono: -468576 Fax: -463507
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

#	participant	country	role	EC contrib. [€]
1	THE UNIVERSITY COURT OF THE UNIVERSITY OF ST ANDREWS  Organization address address: NORTH STREET 66 COLLEGE GATE city: ST ANDREWS FIFE postcode: KY16 9AJ contact info Titolo: Ms. Nome: Trish Cognome: Starrs Email: send email Telefono: -468576 Fax: -463507	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?'