B\"uchi Types for Infinite Traces and Liveness

We develop a new type and effect system based on B\"uchi automata to capture finite and infinite traces produced by programs in a small language which allows non-deterministic choices and infinite recursions. There are two key technical contributions: (a) an abstraction based on equivalence relations defined by the policy B\"uchi automaton, the B\"uchi abstraction; (b) a novel type and effect system to correctly capture infinite traces. We show how the B\"uchi abstraction fits into the abstract interpretation framework and show soundness and completeness.