Venue. TCS
2007
Relational separation logic yang_relational_separation_2007
2003
Glueing and orthogonality for models of linear logic hyland_glueing_2003
We present the general theory of the method of glueing and associated technique of orthogonality for constructing categorical models of all the structure of linear logic: in particular we treat the exponentials in detail. We indicate simple applications of the methods and show that they cover familiar examples.
1995
Nonsymmetric *-autonomous categories barr1995-nonsymmetric-star-autonomous
1987
Linear logic girard_linear_1987
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 has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.