Alternating Krivine Automata

Alternating Parity Krivine Automata (APKA) provide operative semantics to Higher-Order Modal Fixpoint Logic (HFL). APKA consist of ordinary parity automata extended by a variation of the Krivine Abstract Machine. We study their construction and show how any HFL-formula can be converted into an APKA. Time permitting, we also sketch hoe the number and parity of priorities available to an APKA form a proper hierarchy of expressive power as in the modal μ-calculus, which also induces a strict alternation hierarchy on HFL.