Extending a Call-by-Value Calculus Based on Bilateralism with Dynamic Binding Extending a Call-by-Value Calculus Based on Bilateralism with Dynamic Binding

Tatsuya Abe and Daisuke Kimura. Extending a Call-by-Value Calculus Based on Bilateralism with Dynamic Binding. Journal of Applied Logics, 10(4):511–530, 2023.

Bilateral natural deduction has judgments about not only acceptance but also rejection. A typed lambda-calculus corresponding to bilateral natural deduction on the formulae-as-types notion has not only first-class expressions but also first-class continuations. Functions on continuations in the calculus have co-implication types. In this paper, we extend the call-by-value variant of the calculus with dynamic binding. In the extended calculus, we can more delicately operate and observe continuations in the computation. We demonstrate that a language with control operators for delimited continuations can be compiled into the extended calculus.