A Third-Order Representation of the λμ-Calculus
Andreas M. Abel · Electronic Notes in Theoretical Computer Science · 2001
Higher-order logical frameworks provide a powerful technology to reason about object languages with binders. This will be demonstrated for the case of the λμ-calculus with two different binders which can most elegantly be represented using a third-order constant. Since cases of third- and higher-order encodings are very rare in comparison with those of second order, a second-order representation is given as well and equivalence to the third-order representation is proven formally.