[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}