The secret pi calculus is a variant of the pi calculus that features both dynamic and static communication channels; differently from dynamic channels, the scope of static channels cannot be extruded.  This is achieved during the execution by means of a mechanism of accepted/blocked channels in process  rearrangement; the  construction  can be interpreted as a monitored run-time system. In this talk, we present   a type system  for a standard pi calculus that allows to represent the secret channel abstractions through static  and dynamic type modalities for channels (scope). The main aim is to provide a abstract API for  secure message-passing communication : the programmer declares which channels are meant to be secret, the compiler enforces a static scope by means of static type-checking. Towards this direction, we discuss ongoing work on  type inference of static and dynamic types, and attack some examples with the ocaml/z3 implementation.  

Short Bio: Marco Giunti obtained his PhD from Venice University, Italy, and subsequently held post-doc positions at the University of Lisbon, Ecole Polytechnique Palaiseau, NOVA University of Lisbon, and University of Porto. Before joining FCUL as invited professor he was an invited professor at the University of Beira Interior, in the RELiablE And SEcure Computation Group. Marco's main  interests focus on the formal aspects of message-passing concurrent programs, ranging from semantic  theories for program equivalence, to program correctness and security through type systems and program logics, and  program enhancement through  program transformation techniques.