[Prev][Next][Index][Thread]
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