Abstract

Linear logic is the logic of resources which can neither be created nor destroyed—or so common wisdom would dictate. But while tensorial resources are indeed preserved, resources that represent some kind of choice may still be duplicated or destroyed in certain circumstances. For example, the type of booleans, 1 + 1, is equivalent (though not isomorphic!) to the unit type 1, representing “empty truth”.

In this talk, I will describe research being done now with Amr Sabry into a sequent calculus for a reversible logic that fixes these shortcomings. I will also discuss a work in progress that involves adding explicit, irreversible rules into the sequent calculus to get a system that proves the same theorems as linear logic.