Version 1 (modified by sacerdot, 9 years ago) (diff)



The University Paris Diderot is the major pluri-disciplinary University in France. The University gathers 26,000 students, 1,800 researchers and academic staff and 125 research teams covering a wide range of fields. The laboratory PPS (Proofs, Programs, and Systems) is a joint laboratory of University Paris Diderot and the CNRS (Centre National de la Recherche Scientifique) whose research spans from mathematical foundations to open source software development. The main scientific themes of the laboratory are: (1) Mathematical structures of programming, in particular game semantics, linear logic, and algebraic methods, (2) Proof and rewriting theory, in particular type theory, extraction of programs from proofs via realisability interpretations, explicit substitutions, and formal proof developments in Coq (3) Concurrency and modelling, in particular models of concurrent programming, probabilistic systems, and molecular biology modelling. (4) Software tools, in particular web languages and programming and environments for open source software development and distribution.

Role in the project and main tasks

The UPD site will lead the Work Package 2 on the development of an (unverified) prototype compiler. This activity should be completed during the first 18 months of the project. Starting from month 12, it will take up coordination of Work Package 5 (management of complexity assertions and automation of complexity proofs).

Relevant previous experience (resource analysis)

  • EU Project IST-2001-33149 on Mobile Resource Guarantees (2003) (member).
  • Control of Resources and Interference in Synchronous Systems (2003-2006), French national ANR programme on Security and Informatics (coordinator).
  • Parallelism and Security (2006-2009). French ANR programme on Security and Informatics (member).

Staff members involved (UPD)

Roberto Amadio Professor University Paris Diderot
Yann R�gis-Gianas Lecturer/Assistant? professor University Paris Diderot
PostDoc? (12 months) to be hired during year 1
PhD Student (36 months) to be hired

Key person at UPD

Roberto Amadio is Professor at the University of Paris Diderot. Previously he has held positions as Professor at the University of Aix-Marseille 1 and as Research Fellow of CNRS in Nancy and Nice. He holds a PhD from the University of Pisa and an Habilitation from the University of Nancy. He is the author of a monograph on Domains and Lambda-Calculi and of over 50 publications on domain theory, semantics of -calculus and type theory, process calculi, models of migration, protocol analysis and verification, mobile code and resource control. He is a member of the steering committees of the conferences Concurrency Theory, Computer Security Foundation Symposium, and European Joint Conferences on Theory and Practice of Software (ETAPS). He is also responsible for the University Paris Diderot of the Master Parisien de Recherche en Informatique which is the leading Research Master in Informatics in France. He is currently teaching a course on�amadio/Ens/Compilation/syntax analysis and compilers.

Recent publications related to the project comprise:

  1. R. Amadio, S. Coupet-Grimal, S. Dal Zilio, L. Jakubiec. A functional scenario for bytecode verification of resource bounds. In Proc. Computer Science Logic, Springer LNCS 3210 , 2004.
  2. R.�Amadio. Synthesis of max-plus quasi-interpretations. Fundamenta Informaticae, 65(1-2):29-60, 2005.
  3. R.�Amadio, S.�Dal-Zilio. Resource control for synchronous cooperative threads. Theoretical Computer Science, 358:229-254, 2006.