Aalborg University, Denmark
4pm Thursday 17th April 2008
Room 2511, JCMB, King's Buildings
Note nonstandard day
We present a correspondence type/effect system for authenticity in a pi-calculus with polarized channels, dependent pair types and effect terms and show how one may, given a process P and an a priori type environment E generate constraints that are formulae in the Alternating Least Fixed-Point (ALFP) logic. We then show how a reasonable model of the generated constraints yields a type/effect assignment such that P becomes well-typed wrt. E if and only if this is possible. The formulae generated satisfy a finite model property; a system of constraints is satisfiable if and only if it has a finite model. As a consequence, we obtain the result that type/effect inference in our system is polynomial-time decidable.
Joint work with Andy Gordon (Microsoft Research Cambridge) and René Rydhof Hansen (Aalborg University)