Sections:

Latest news:

December 15, 2010:
Last meeting of the Parsec project.

Read more »

June 28, 2010:
Eight meeting of the Parsec project.

Read more »

December 15, 2010 --- MSR-INRIA Joint Lab, Orsay

Program

10h-10h30 meeting
10h30-11h10 D. Varacca Parallel extrusion in the pi-calculus
11h10-11h50 G. Petri TBA
11h50-12h30 M. Dogguy TBA
12h30-14h lunch
14h-14h40 D. Pichardie Secure the Clones
14h40-15h20 K. Bhargavan Type-checking higher-order security libraries
15h20-15h40 pause
15h40-16h20 F. Zappa Nardelli Relaxed memory concurrency and verified compilation
16h20-17h Panel what's next?

Participants

G. Petri, F. Zappa Nardelli, I. Castellani, T. Rezk, G. Boudol, T. Jensen, M. Dogguy, D. Varacca, D. Pichardie.

June 28, 2010 --- INRIA, Sophia Antipolis

Program

10h30-11h meeting
11h-11h45 A. Madet An affine-intuitionistic system of types and effect: confluence and termination
11h45-12h30 T. Rezk Code injection
12h30-14h discussion and lunch
14h-14h45 G. Boudol A type system to guarantee sequential consistency in RMO + barriers
14h45-15h30 P. Pawan A daemonic x86-TSO emulator
15h30-16h discussion and pause
16h-16h45 N. Guts Type inference for F7
16h45-17h30 I. Castellani Session types for access and information flow control

Participants

A. Madet, G. Petri, F. Zappa Nardelli, J.J. Lévy, I. Castellani, T. Rezk, G. Boudol, T. Jensen, M. Dogguy, N. Guts, F. Dabrowski, B. Serpette, P. Pawan, Z. Luo, P. Attar, J. Grand, T. Gazagnaire.

January 29, 2010 --- INRIA, Paris

Program

10h15-10h40 meeting
10h40-11h20 D. Pichardie Secure Cloning
11h20-12h00 G. Petri A theory of speculative computations
12h-13h30 discussion and lunch
13h30-14h10 G. Manzonetto Resource calculi: some syntax, some semantics
14h10-14h50 G. Castagna Contracts for Mobile Processes
14h50-15h20 discussion and pause
15h20-16h00 T. Rezk Security in Hop web applications
16h00-16h40 G. Le Guernic Cryptographically Secured Information Flows of Distributed Programs

Participants

G. Castagna, G. Petri, F. Zappa Nardelli, J.J. Lévy, I. Castellani, T. Rezk, G. Boudol, T. Jensen, R. Amadio, G. Manzonetto, M. Dogguy, J. Planul, N. Guts, D. Pichardie, G. Le Guernic, A. Bucciarelli

June 4, 2009 --- INRIA Sophia-Antipolis

Program

10h-11h F. Zappa Nardelli Like Types
11h-12h J. Alglave The Power memory model
12h-13h30 discussion and lunch
13h30-14h15 G. Boudol A semantics without deadlocks
14h15-15h B. Serpette Qui sème la fonction récolte le tuyau typé
15h-15h30 discussion and pause
15h30-16h15 F. Dabrowski Iteration sensitive escape analysis
16h15-17h00 R. Amadio Termination of lambda-calculus with references

Participants

F. Boussinot, G. Petri, F. Zappa Nardelli, J.J. Lévy, F. Dabrowski, I. Castellani, T. Rezk, G. Boudol, T. Jensen, J. Alglave, L. Maranget, B. Serpette

January 8, 2009 --- MSR-INRIA Joint Lab, Orsay

Program

11h30-12h C. Hurlin Automatic parallelization based on proof rewriting
12h-12h30 F. Boussinot The ANR PARTOUT project
12h30-14h30 discussion and lunch
14h30-15h T. Rezk A compiler for security
15h-15h30 R. Amadio On convergence sensitive bisimulation
15h30-16h F. Dabrowski Towards a formal semantics of MIDP graphical user interfaces
16h-16h30 discussion and pause
16h30-17h00 D. Pichardie A certified data race analysis for a Java-like language
17h00-17h30 C. Hurlin Size does matter

Participants

F. Boussinot, G. Petri, F. Zappa Nardelli, J.J. Lévy, D. Pichardie, F. Dabrowski, I. Castellani, C. Hurlin, T. Rezk, G. Boudol, T. Jensen, L. Maranget

June 9, 2008 --- IRISA, Rennes

Program

11h-1130h F. Zappa Nardelli The Intel 64/ia-32 relaxed memory model
11h30-12h D. Varacca The meaning of causal labelled bisimulations
12h-12h30 G. Boudol Secure information flow as a safety property
12h30-14h30 discussion and lunch
14h30-15h G. Pietri On relaxed memory models
15h-15h30 F. Dabrowski Formalisation of static analysis for multithreaded Java
15h30-16h J. Vitek Flexible Task Graphs
16h-16h30 discussion and pause
16h30-17h00 C. Hurlin Separation logic for a Java-like language
17h00-17h30 F. Zappa Nardelli Oracle Semantics for Concurrent Cminor (.pptx)

Participants

G. Pietri, G. Boudol, C. Hurlin, I. Castellani, F. Boussinot, F. Dabrowski, D. Pichardie, T. Jensen, R. Amadio, M. Dogguy, D. Varacca, J. Vitek, F. Zappa Nardelli.

December 13, 2007 --- PPS, U. Paris 7

Program

10h-11h F. Zappa Nardelli Ott: effective tool support for the working semanticist
11h-12h G. Barthe Certificate translation for optimizing compilers
12h-13h F. Dabrowski Data races in Java and static analysis
13h-14h lunch
14h-15h G. Boudol Typing termination in a higher-order, concurrent, imperative language
15h-16h G. Castagna A theory of contracts for web services
16h-17h M. Dogguy Linear usages in signal-based communication

Participants

F. Boussinot, G. Le Guernic, F. Dabrowski, D. Pichardie, G. Castagna, D. Kesner, R. Di Cosmo, G. Barthe, O. Danvy, E. Giacchino, R. Amadio, M. Dogguy, F. Zappa Nardelli, G. Boudol, I. Castellani, M. Kolundzija, C. Hurlin, J-J. Lévy, D. Varacca.

June 20, 2007 --- MSR-INRIA Joint Lab, Orsay

Program

10h-10h30 breakfast ParSec organisation
10h30-11h A. Appel Threads can be implemented as a (semantic) library
11h-11h30 J. Alglave Certified symbolic execution with separation logic.
11h30-12h C. Hurlin Permission based verification of dara race freeness for lock free programs
12h-13h30 lunch
13h30-14h I. Castellani State-oriented noninterference for CCS
14h-14h30 D. Varacca Event structure semantics for untyped pi-calculus.
14h30-15h R. Amadio Determinacy in a synchronous pi-calculus
15h-15h30 pause
15h30-16h C. Fournet Secure implementations for Typed Session Abstractions
16h-16h30 G. Le Guernic Automaton-based Confidentiality Monitoring of Concurrent Programs.
16h30-17h M. Kolundzija Acces control and declassification.

Participants

J. Alglave, F. Boussinot, G. Le Guernic, F. Dabrowski, A. Appel, D. Pichardie, T. Rezk, C. Fournet, R. Amadio, M. Dogguy, F. Zappa Nardelli, O. Tardieu, G. Boudol, I. Castellani, M. Kolundzija, M. Huisman, C. Hurlin, J-J. Lévy, D. Varacca.

February 2, 2007 --- INRIA Sophia-Antipolis

Program

9h30-10h30 G. Boudol Research on Security in the Mimosa research team
10h30-11h pause
11h-12h G. Barthe Les travaux dans l'équipe Everest
12h-12h30 J-J. Lévy History based flow analysis
12h30-14h déjeuner
14h-14h45 D. Pichardie A certified static analyser in constructive logic
14h45-15h15 F. Besson Language-based access control
15h15-16h R. Amadio A synchronous pi-calculus
16h-16h15 pause
16h15-17h F. Zappa Nardelli Concurrent CMinor
17h-17h30 D. Varacca Déterminisme et structures d'événements dans le pi-calcul

Participants

R. Amadio, G. Barthe, F. Besson, G. Boudol, F. Boussinot, S. Cavadini, I. Castellani, F. Dabrowski, M. Huisman, C. Hurlin, T. Jensen, M. Kolundzija, J-J. Lévy, G. Petri, D. Pichardie, T. Rezk, O. Tardieu, D. Varacca, F. Zappa Nardelli.