# Understanding $\lambda \mu$-calculus in more programming way

I am learning $$\lambda \mu$$-calculus (self-study).

I learned it because it seems very useful for understanding Curry-Howard correspondence (e.g understanding the connection between classical logic and intuitionistic logic)

I searched the internet, there is some information about $$\lambda \mu$$-calculus on Wikipedia, but it does not explore it further (at time of writing). https://en.wikipedia.org/wiki/Lambda-mu_calculus

Is there any more programming way to interpret the intuition behind $$\lambda \mu$$-calculus?

For example:

In $$\lambda \mu$$-calculus, there are two additional terms called $$\mu$$-abstraction $$\mu \delta .T$$ and named term $$[\delta]T$$.

Can I think $$\mu$$-abstraction as a $$\lambda$$-abstraction which waiting for some continuation $$k$$ (here, is $$\delta$$)?

What's the meaning of the named term?

How does it connect to call/cc?

Can I find the corresponding roles in some programming language (e.g. Scheme)?

PS: I can understand $$\lambda$$-calculus, call/cc in Scheme, and CPS-Translation, but I still cannot clearly understand the intuition behind $$\lambda \mu$$-calculus.

Very thanks.

• Following the links from Wikipedia, you can find a paper by Wadler, which has better description of the calculus: homepages.inf.ed.ac.uk/wadler/papers/dual-reloaded/… Commented Jul 1, 2020 at 5:55
• From the paper: “The computational interpretation of a μ- abstraction μα.S is to bind the covariable α and then evaluate statment S; if during evaluation of S the covariable α is applied to a value, then that value is returned as the value of the μ-abstraction; this is similar to the behaviour of callcc in Scheme.” Commented Jul 1, 2020 at 5:57