Extending computational trinitarianism

Computational trinitarianism is the view that a single notion of computation has three different manifestations: in logic as proofs, in typed λ-calculus as programs, and in category theory as morphisms. This idea has traditionally been closely associated with intuitionistic logic but here we argue that the connection is not exclusive. We provide a logician friendly, self-contained introduction to this topic by presenting the trinities for linear, affine, and relevant logic. The ground we set for that goal is then used to show how to obtain paraconsistent trinities by including the De Morgan negation.