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?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.