Linear logic

   page       BibTeX_logo.png   
Jean-Yves Girard
Theoretical Computer Science 50(1), pages 1-102

The familiar connective of negation is broken into two operations: linear negation, which is the purely negative part of negation, and the modality “of course”, which as the meaning of a reaffirmation.
Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.