In case anyone is turned off by the expectation of wishy-washy flim-flam, it's worth noting that Graham Priest may be a professor of philosophy, but is most well known for his work in logic, particularly in non-standard logics (i.e. not propositional or predicate logic) that allow non-boolean truth values, or weaken or remove some of the axioms of classical logic.
I assume that what's relevant here will be his work on paraconsistent logics (which allow contradictions) but I think an equally interesting line of work is linear logics. It's of interest to computer scientists because of its relationship to linear type theory (in the same way that the Curry-Howard correspondence links type theory and classical logic) and because it has close relationships with quantum computing.
In particular, you are not allowed to delete or duplicate elements/propositions/types (corresponding to physical processes that cannot arbitrarily create or destroy particles, the "no deletion theorem" and "no cloning theorem" of quantum information theory), so functions of the type
duplicate :: a -> (a, a)
and
delete :: a -> ()
are not allowed in a linear type system. Practically, this means that many operations can be optimized by the compiler to in-place mutations, because it is guaranteed that there is only ever one reference to a particular object.
I assume that what's relevant here will be his work on paraconsistent logics (which allow contradictions) but I think an equally interesting line of work is linear logics. It's of interest to computer scientists because of its relationship to linear type theory (in the same way that the Curry-Howard correspondence links type theory and classical logic) and because it has close relationships with quantum computing.
In particular, you are not allowed to delete or duplicate elements/propositions/types (corresponding to physical processes that cannot arbitrarily create or destroy particles, the "no deletion theorem" and "no cloning theorem" of quantum information theory), so functions of the type
and are not allowed in a linear type system. Practically, this means that many operations can be optimized by the compiler to in-place mutations, because it is guaranteed that there is only ever one reference to a particular object.