[Prev][Next][Index][Thread]
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
http://www.dcs.qmw.ac.uk/~pym/Paperspage/recent.html
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?