Personal tools
You are here: Home Events Abstract Archives 2007-2008 Type Inference for Correspondence Types

Type Inference for Correspondence Types

Hans Hüttel 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)

Document Actions