Re: Higher-order linear logic

You may find the paper by Ishtiaq and Pym,
`A Relevant Analysis of Natural Deduction',
J. Logic. Computat. 8(6) 809-838 1998 of
some interest. It gives a dependent type theory
with a linear dependent function space. I can also
point you to papers on its semantics if you'd like.

My draft monograph, `The Logic of Bunched Implications',
is avaialable at


along with the papers mentioned above. It contains the aforesaid
material presented in a broader, more mature context (and has
a few known typos fixed).

Kind regards,

    David Pym

Prof. David J. Pym (Prof. of Logic & EPSRC Advanced Fellow),
Department of Computer Science,
Queen Mary,
University of London,
London E1 4NS, England, U.K.

  Tel: +44 (0)20 7882 5237   Mob: +44 (0)7 770 941 725
  Fax: +44 (0)20 8980 6533  Room: CS/426
Email: pym@dcs.qmw.ac.uk     WWW: http://www.dcs.qmw.ac.uk/~pym

Daniel Wang wrote:

> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
> Does anyone have any pointers for higer-order linear logics?
> i.e. something like Church's higher-order logic with linear
> implication and linear abstraction? i.e. F-Omega with linear
> implication, and linear type constructors? Have people studied such
> systems and are they even sensible?