lambda-bar-mu-mu-tilde calculus

The calculus is a term assignment system for the sequent calculus.

The calculus has two kinds of variables: term variables and context variables . In addition, it has three syntactic categories: commands , producers , and consumers .

Intuitively, a producer is like an expression in a typical programming language: it evaluates to a value. Dually, a consumer is like a context or a continuation: it awaits a value. Commands are where computation happens: says to evaluate the value expression in the context .

binds the current context to a variable and executes a command: This is rather like call/cc, but with an explicit context rather than an implicit one.

Dually, binds the expression currently being evaluated to a variable and executes a command: Thus, is sort of like a function construct, although it might be better to think of it as a let construct with a “hole” where the definition should be; i.e., .

Finally, introduces functions, as usual; the dual construct is the dot . might be read as ; or, in English, “supply as an argument to the expression currently being evaluated, and then continue in the context ”.

It is instructive to consider how the command should compute. The following seems perfectly reasonable: However, we already have a rule that can perform substitution on term variables—namely, . Can we express