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?