CO-TYPES · Types for Communicating Software Systems
FP6 — Marie Curie Actions (Human Resources and Mobility)
- Duration
- 2007-02-01 → 2009-01-31
- EU contribution
- €152,242
- Participants
- 1
- Scheme
- EIF
Lines connect the coordinator with its partners.
Results in brief
Final Activity Report Summary - CO-TYPES (Types for Communicating Software Systems)
Types are used in programming languages to make sure that the programmer doesn't accidently confuse apples and oranges, or more likely booleans and integers, since programs which do may crash or provide backdoors to criminals. In the research on dependently typed programming, of which COTYPES is a part, we try to shift the scope of what you can do with types further, indeed we use very expressive type system which can express any property of the program in its type. Here program verification and programming meet, in a beneficial way: the compiler can check that we aren't lying and we can "pay as we go", we can gradually increase the guarantees given by the program's types. In COTYPES we focussed on a practically very important aspect: providing the means to use this technology to deal with infinite, i.e. never-ending computations, as they occur in network protocols and distributed computations. We encountered some serious technical issues with the approaches currently used in system like the French COQ proof assistant and the Swedish Agda programming language and development environment and proposed a very small core language (PiSIgma) which overcomes this problem. We also published a paper where we show how dependent types can be used to encode data format and make sure that they are used properly.
Data: CORDIS, © European Union
Project objective
This research directly addresses the need for software technology to develop reliable and robust communicating computer systems. It directly responds to the FP6 objective on Communication, computing and software technologies (Council decision 2002/834/EC) to improve the performance, reliability, cost-efficiency, functionality and adaptive capabilities of communications and computing technologies so as to meet the growing needs of application. We shall combine skills and experience from two long-standing research teams, the Coq (proof assistant) team in France and the Epigram (programming language) team in Britain. Coq and Epigram share a broadly compatible basis but have developed in distinct directions with complementary strengths.We must share our understanding to face the challenges ahead, hence we seek two years' funding for Nicolas Oury, an outstanding young researcher from the Coq team in Paris (Orsay), to do post-doctoral research with the Epigram team in Nottingham, studying the construction of reliable communicating software systems. Oury's doctoral research is crucial for the success of this project, as it lays an essential and previously missing piece of the theoretical foundations for reasoning about communicating processes. Joining the group in Nottingham will be extremely beneficial for Oury's future research career due to the complementarity of the approaches of the French and British groups and the strength of the Nottingham team in working on applications of Type Theory in Programming.Our objective is to develop programming language and tool support geared towards productivity and reliability of communicating software systems. Our approach is to extend the existing Epigram platform, which already provides language and tool support for reliable algorithmic programming. We shall adopt the necessary structures required to express and work with the kinds of guarantees we require from communicating software.
Original text from CORDIS.
Participants
- UNIVERSITY OF NOTTINGHAM · NOTTINGHAMCoordinatorUnited Kingdom
Links
Data: CORDIS, © European Union