This project (SI05-02) is supported by the PRA program of AFCRST.

Objectives

The long term scientific objective of the research proposed here is to develop robust and sound techniques for the challenges in computation, which cover a wide range of application, such as embedded systems and biological systems. A deep understanding of the underlying computational phenomena is needed, which involves, in our sense, the development of the dedicated mathematical foundations, such as process algebra and type theory.

Partners and contacts

1. BASICS (Laboratory for Basic Studies in Computing Science), Shanghai Jiaotong University, Shanghai: Yuxi FU.
2. LCS (Laboratory of Computer Science), Institute of Software, Chinese Academy of Sciences, Beijing: Ying JIANG.
3. The Laboratory for Programming Logic, Nanjing University: Fangmin SONG.
4. VERIMAG, Université Joseph Fourier: Jean-François MONIN.
5. PPS, Université Denis Diderot: Pierre-Louis CURIEN.

The partners share a common interest on software development methods based on firm and sound mathematical ground, especially type theory and algebraic computational models. A previous cooperation, ended two years ago, led by the Institute of Software in Beijing and Paris 7/PPS, placed the emphasis on the logical foundations. The new cooperation is led by Jiaotong University/BASICS at Shanghai and University Joseph Fourier/VERIMAG at Grenoble, and focuses on proof engineering, mobility and the modeling of biological processes.

Research Program

In this project, we propose to advance the understanding of the concurrency theory, type theory and their roles in applications on security and biological processes by carrying out investigations in the following aspects:

• We wish to design and develop languages for modeling biological processes, such as DNA computing and protein computing, using the concurrency theoretical framework.. The core languages, such the as kappa calculus, proposed by Vincent Danos of PPS seem more suitable for theoretical study, while the frameworks developed in Fu Yuxi's group are closer to the problems being modeled. The ultimate goal is to build a process calculus that could model and analyze most aspects of the biology computing. BASICS and PPS are interested in mutual encodings, and the possibility to define equivalences (bisimulation) enabling us to reason at a behavioral level, not only a descriptive one. The encodings should naturally respect the equivalences. Zhang Min has done preliminary work in this direction. Furthermore, we hope to develop an automatic verification tool (mainly at BASICS) that would help to predict the results of biological experiments. Biologists could use the tool to design biological experiments.
• BASICS and VERIMAG intend to study the security protocols in a formal method approach. Process calculi are used to model protocols, which together with model checking, bisimulation and type checking, are known to be useful in the design and analysis of security protocols. In particular, we will study the fairness and the anonymity issues in the framework of Ambient Calculus. Two models are to be discussed. One is FA, the Calculus of Fair Ambient, designed with considerations to fair interactions. The other is AA, the Calculus of Anonymous Ambient, which formalizes the anonymity in a distributed scenario.
• VERIMAG and the Laboratory for Programming Logic of Nanjing are also interested in a type theoretical formalization of the definition and semantics of the various calculi considered in items 1 and 2. It is a natural extension of the work started at VERIMAG on the join calculus. Then, using the Coq proof assistant, we can expect to get a software support for justifying translations, equivalences and so on. This work will of course involve a close cooperation with BASICS and PPS.
• The last part of this project is more specifically devoted to theoretical developments in type theory and lambda-calculus. It has been known for some time that there is a correspondence between the datatypes of the programming languages and the types of the polymorphic lambda-calculus. However the types of the polymorphic lambda-calculus used in this correspondence are very simple. It seems that more involved types of the polymorphic lambda-calculus correspond to a kind of "higher-order datatypes". LCS and PPS propose to investigate a large class of types in polymorphic lambda and to determine those types for which elements can be described by a grammar. This work builds on our previous work where an inhabitation algorithm for such types was discussed.

This document was translated from L^AT_EX by H^EV^EA.