μμ̃-calculus

if the variable x stands for an unknown input in a command c, then the input abstraction μ̃x.c is a co-term that, when given a place to draw information, will bind that location to the input channel x while running c. Dually, if the co-variable α stands for an unknown output in a command c, then the output abstraction μα.c is a term that, when given a place to send information, will bind that location to the output channel α while running c.

Zena M. Ariola, Aaron Bohannon, and Amr Sabry. Sequent calculi and abstract machines.

Zena M. Ariola, Aaron Bohannon, and Amr Sabry. Sequent calculi and abstract machines.

https://www.cs.indiana.edu/~sabry/papers/sequent.pdf

The reductions corresponding to the abstract machine transitions must occur at a bounded depth from the root of the syntax tree.

Although languages based on lambda-calculi have been successful in supporting reasoning about high-level programs, in this paper we focus on sequent calculi. We show that sequent calculi are more suitable for reasoning about abstract machines since they allow one to define an evaluator for terms in a tail-recursive fashion, thus satisfying the above criterion.

Value Recursion in Monadic Computations

https://digitalcommons.ohsu.edu/cgi/viewcontent.cgi?article=1163&context=etd

This thesis addresses the interaction between recursive declarations and computational effects modeled by monads.