## A Formulae-as-Types Interpretation of Subtractive Logic

A Formulae-as-Types Interpretation of Subtractive Logic

We present a formulae-as-types interpretation of Subtractive Logic (i.e. bi-intuitionistic logic). This presentation is two-fold: we first define a very natural restriction of the lambda-Î¼-calculus which is closed under
reduction and whose type system is a constructive restriction of the Classical Natural Deduction. Then we extend this deduction system conservatively to Subtractive Logic. From a computational standpoint,
the resulting calculus provides a type system for first-class coroutines (a restricted form of first-class continuations).

Yet another connection between subtractive logic and control. I remember the author mentioned on LtU, but I cannot find any citations.

## Comment viewing options

### A confluent lambda-calculus with a catch/throw mechanism

To those find this paper too hard but interesting, I recommend A confluent lambda-calculus with a catch/throw mechanism as a starter.