An environment machine for the λμ-calculus
Philippe de Groote · Mathematical Structures in Computer Science · 1998
We introduce a natural deduction-like formalisation of Parigot's λμ-calculus. From this, we derive an environment machine that allows any well-typed λμ-term to be reduced to its weak head normal form. The soundness and completeness of the machine is proved.