Types, Processes and Applications to Security and Biological Systems
This project (SI05-02) is supported by the PRA program of AFCRST.
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
BASICS (Laboratory for Basic Studies in Computing Science), Shanghai
Jiaotong University, Shanghai: Yuxi FU.
- LCS (Laboratory of Computer Science), Institute of Software, Chinese
Academy of Sciences, Beijing: Ying JIANG.
- The Laboratory for Programming Logic, Nanjing University: Fangmin SONG.
- VERIMAG, Université Joseph Fourier: Jean-François MONIN.
- 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.
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
- 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
- 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 LATEX by