Re: Higher-order linear logic

Daniel Wang asked:
> Does anyone have any pointers for higer-order linear logics?

I would like to know of any such work as well. I believe this would be 
quite difficult, so the approach taken by Maietti, de Paiva, Ritter, and 
me is to try to combine the usual first-order linear logic with higher 
order logic by making the atoms of LL formulae in HOL. My student Mike 
Squire has implemented this system in Isabelle. This seems to work 
well. A preliminary version of this system is described in a paper
available at ftp://ftp.dcs.warwick.ac.uk/people/Sara.Kalvala/ll-hol.ps

Cheers, - Sara

> 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?

Sara Kalvala                            Department of Computer Science
sk@dcs.warwick.ac.uk                    University of Warwick
Tel: +44 24 7652 3179                   Coventry   CV4 7AL    UK
Fax: +44 24 7657 3024                   http://www.dcs.warwick.ac.uk/~sk