Type inference for correspondence types

We present a type and eï¬€ect system for proving correspondence assertions in a Ï€-calculus with polarized channels, dependent pair types and eï¬€ect terms. Given a process P and a type environment E, we describe how to generate constraints that are formulae in the Alternating Least Fixed-Point (ALFP) logic. A reasonable model of the generated constraints yields a type and eï¬€ect assignment such that P becomes well-typed with respect to E if and only if this is possible. The formulae generated satisfy a ï¬nite model property; a system of constraints is satisï¬able if and only if it has a ï¬nite model. As a consequence, we obtain the result that type and eï¬€ect inference in our system is polynomial-time decidable.

That's a mouthful. The part of the paper that perked my virtual ears up:

Most importantly, our approach is general in nature; the encoding of types and terms does not depend on the rules of the type system. For this reason, our approach appears a natural candidate for obtaining similar type inference results for type systems such as [9], where correspondences concern formulas in an arbitrary authorization logic and the underlying process calculus includes cryptographic operations, and type systems for secrecy properties such as [12]. The possibility of such ramiï¬cations is currently under investigation.

[9] is A type discipline for authorization policies, which is followed up by Type-checking zero knowledge. The upshot is that it might be possible to have reasonable type inference support for a dependent type- and effect system with cryptographic operations supporting some of the most powerful privacy and security primitives and protocols currently known. I find this very exciting!

## Recent comments

6 hours 53 min ago

7 hours 41 min ago

1 day 2 hours ago

1 day 3 hours ago

1 day 3 hours ago

1 day 19 hours ago

1 day 20 hours ago

2 days 4 hours ago

3 days 1 hour ago

3 days 7 hours ago