# Type System Of $\lambda\mu$-Calculus

reading this paper on CPS-tranformation from the $$\lambda\mu$$-calculus, I'm a bit confused about the type system presented:

• Why second-order formulas in the types? Is this according to the Curry-Howard interpretation?
• What kind of second-order formulas are permitted here, can $$X$$ be any arbitrary n-ary relational symbol?
• Am I reading this correctly, that the quantifier introduction / elimination rules only apply to non-indexed formulas?
• Is there a relation between the $$\lambda$$-variables in the terms (resp. the indices of the formulas in $$\Gamma$$) and the variables in the formulas?
• As far as I can see, the only way for a $$\lambda\mu$$-formula to have a type is that any occurence $$[\alpha]$$ is directly preceded by some $$\mu\beta$$ since $$[\alpha]M$$ has a type of the form $$\Gamma\vdash\Delta$$ and the only typing rule that can deal with this form (no non-indexed formula $$A$$) is $$\mu$$-introduction. Is that correct?