Gordon and Jeffrey developed a type system for checking correspondence
assertions. The correspondence assertions, proposed by Woo and Lam,
state that when a certain event (called an ``end'' event)
happens, the corresponding ``begin'' event must have occurred before.
They can be used for checking authenticity in communication protocols.
In this paper, we refine Gordon and Jeffrey's type system and
develop a polynomial-time type inference algorithm,
so that correspondence
assertions can be verified fully automatically, without
any type annotations.
The main key idea that enables polynomial-time type inference
is to introduce fractional effects; Without the fractional effects,
the type inference problem is NP-hard.