[Prev][Next][Index][Thread]

Re: Higher-order linear logic

In the context of proof search (logic programming), higher-order
quantification has long been use in various applications.  The earliest
uses were with Horn clauses [nadathur90jacm] and intuitionistic logic
[miller91apal].  Later versions mixed higher-order quantification (as in
Church's Simple Theory of Types) with intuitionistic linear logic
[hodas94ic] and all of linear logic [miller96tcs].   Numerous examples
mixing higher-order quantification with linear logic are illustrated in
these last two papers.  Most of these examples focus on the
specification of computation systems involving state and
synchronization.

-Dale Miller
http://www.cse.psu.edu/~dale/
ftp://ftp.cis.upenn.edu/pub/papers/miller/recentpapers.html

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?

@Article{nadathur90jacm,
  Author = "Gopalan Nadathur and Dale Miller",
  Title = "Higher-order {Horn} Clauses",
  Journal = "Journal of the ACM",
  Volume = "37",
  Number = "4",
  Month = "October",
  Year = 1990,
  Pages = "777-814"}

@Article{miller91apal,
  Author = "Dale Miller and Gopalan Nadathur and Frank Pfenning and
            Andre Scedrov",
  Title = "Uniform Proofs as a Foundation for Logic Programming",
  Journal = "Annals of Pure and Applied Logic",
  Year = "1991",
  Volume = "51",
  Pages = "125-157"}

@Article{hodas94ic,
  Author = "Joshua Hodas and Dale Miller",
  Title = "Logic Programming in a Fragment of Intuitionistic Linear
Logic",
  Journal = "Information and Computation",
  Year = "1994",
  Volume={110},
  number={2},
  pages={327-365}}

@Article{miller96tcs,
  Author = "Dale Miller",
  Title = "Forum: A Multiple-Conclusion Specification Language",
  Journal = "Theoretical Computer Science",
  Year = "1996",
  pages={201--232},
  month=sep,
  volume=165,
  number=1}