ParticipantsThe Panda project is composed of 4 academic research partners (INRIA Saclay, CEA LIST, pôle parisien, pôle méditerranéen) and 1 industrial partner (Airbus). 
INRIA Saclay
The Institut National de Recherche en Informatique et Automation (INRIA) participates with members based at its Saclay site, belonging to the following INRIA reasearch projectsteams: COMETE: the INRIA project called COMETE focuses on the design, implementation and applications of formal languages for mobile, secure, stochastic and distributed systems of the kind considered by Panda. Its members are particularly interested in formal languages based on process calculi.
PARSIFAL: the PARSIFAL projectteam aims at elaborating methods and tools for specifying and reasoning about computation systems, such as, for example, compilers, security protocols, and concurrent programs. A central challenge here is proving properties of programs that manipulate other programs.

People involved:

CEA LIST
The Commissariat à l'Energie Atomique (CEA) participates with members from its LIST laboratory, in particular with its team MeASI (Modélisation et Analyse des Systèmes en Interaction). The MeASI team focuses on theoretical research on methods for static analysis, along with the development of applications of related software tools. The ALCOOL group (which is also the name of the software developed by the group) is specialized in the analysis of concurrency and parallelism through techniques coming from directed algebraic topology. Together with this, the ALCOOL group has also expertise in software development (mostly using OCaml).
Within the Panda project, the ALCOOL group will compare its approach to concurrency to other more traditional approaches, which do not make explicit use of topological notions. The Panda project is also an opportunity to confront the ALCOOL toolbox with new case studies originating from the industrial world (in particular those provided by Airbus), in order to enhance its development. The development of the ALCOOL software has been supported for several years by EDF, and is at present going towards the introduction of libraries (to be developed within the Panda project) based on the most recent advances in the domain of directed albegraic topology and concurrency. 
People involved:


Pôle parisien
The pôle parisien is a group of researchers belonging to laboratories situated for the most part in the Paris area. It is coordinated by Université Paris Nord  Paris 13. LIPN: The Laboratoire d'Informatique de Paris Nord (LIPN) is the coordinator of the pôle parisien. LIPN plays a major role in research in computer science within the northern Paris area; in particular, the Panda project touches several topics which are developed at LIPN within its Logic, Computation, and Reasoning team. These include linear logic proof theory, interaction nets and, more generally, rewriting theory, and all their applications to concurrency. PPS: The laboratory Preuves, Programmes et Systèmes federates the energies of researchers coming from different cultures (computer science and mathematical logic) to work on the logical foundations of programming languages and distributed systems. Within Panda, PPS contributes with research spanning from logic (and, in particular, proof theory) to category theory, from homology and homotopy to probability theory, with the aim of providing a clearer understanding of distributed programs and guaranteeing their correctness. LSV: The Laboratoire Spécification et Vérification (LSV) is the computer science laboratory of ENS Cachan. LSV devotes most of its research efforts to the study of the specification and verification of critical systems, with the aim of developing languages and formal methods for expressing and proving correctness of those systems. LSV participates to Panda with members of its research group INFINI, which focuses on verifying infinite systems: programs that manipulate unbounded values, recursive communicating processes, parametrized systems. Members of the INFINI group also develop software tools for program verification; we mention in particular the following, whose development is relevant to the Panda project:
LIP and LAMA: Even though they are not situated in the Paris area, the Laboratoire de l'Informatique du Parallélisme (LIP, ENS Lyon) and the Department of Mathematics of the Université de Savoie (LAMA) contribute to the Panda project with research in the main theoretical fields developed by the pôle parisien. In particular, researchers at LIP and LAMA have a specific expertise in proof theory, games semantics, and formal semantics of concurrent programming languages. 
People involved:


Pôle méditerranéen
The pôle méditerranéen comprises researchers belonging to laboratories situated in Marseille. It is coordinated by Université de Provence  AixMarseille 1. The two laboratories involved are the Laboratoire d'Informatique Fondamentale (LIF, Université AixMarseille 1, the coordinator of the pôle méditerranéen) and the Institut de Mathématiques de Luminy (IML, Université AixMarseille 2). The contribution of the Panda members belonging to the pôle méditerranéen is mostly theoretical, and is focused on the following research axes:

People involved:
