Author name cluster

Jean-Baptiste Joinet

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

1 author row

TCS Journal 2003 Journal Article

Computational isomorphisms in classical logic

Vincent Danos
Jean-Baptiste Joinet
Harold Schellinx

All standard ‘linear’ boolean equations are shown to be computationally realized within a suitable classical sequent calculus LK p η. Specifically, LK p η can be equipped with a cut-elimination compatible equivalence on derivations based upon reversibility properties of logical rules. So that any pair of derivations, without structural rules, of F⇒G and G⇒F, where F, G are first-order formulas ‘without any qualities’, defines a computational isomorphism.

Details DOI

I&C Journal 2003 Journal Article

Linear logic and elementary time

Vincent Danos
Jean-Baptiste Joinet

A subsystem of linear logic, elementary linear logic, is defined and shown to represent exactly elementary recursive functions. Its choicest part consists in reducing the deductive power of the exponential, also known as the “bang, ” which, in linear logic, is in charge of controlling duplication in the cut-elimination process.

Details DOI