Proof-theoretically, it provides a well-behaved formulation of classical natural deduction.
One of the main goals of this extended calculus is to be able to describe expressions corresponding to theorems in classical logic.
However with these new operators one is able to write terms that have the type of, for example, Peirce's law.
[2] The three forms of expressions in lambda calculus are as follows: In addition to the traditional λ-variables, the lambda-mu calculus includes a distinct set of μ-variables, which can be understood as continuation variables.
For a closer correspondence with conventional formalizations of control operators, the distinction between named and unnamed terms can be abolished, meaning that [α]M is of the same sort as other lambda-expressions and the body of μ-abstraction can also be any expression.