\begin{thebibliography}{10}

\bibitem{Bar90}
R.~Barbuti, P.~Mancarella, D.~Pedreschi, and F.~Turini.
\newblock {A} transformational approach to negation in logic programming.
\newblock {\em Journal of Logic Programming}, 8:201--228, 1990.

\bibitem{Bruscoli94}
P.~Bruscoli, F.~Levi, G.~Levi, and M.~C. Meo.
\newblock Compilative constructive negation in constraint logic programs.
\newblock In S.~Tison, editor, {\em Proc. Trees in Algebra and Programming -
  CAAP'94, 19th International Colloquium}, volume 787, pages 52--76. Springer,
  1994.

\bibitem{Cervesato96lics}
I.~Cervesato and F.~Pfenning.
\newblock A linear logical framework.
\newblock In E.~Clarke, editor, {\em Proceedings of the Eleventh Annual
  Symposium on Logic in Computer Science}, pages 264--275, New Brunswick, New
  Jersey, July 1996. IEEE Computer Society Press.

\bibitem{Comon91}
H.~Comon.
\newblock Disunification: a survey.
\newblock In J.-L. Lassez and G.Plotkin, editors, {\em Computational Logic}.
  MIT Press, Cambridge,MA, 1991.

\bibitem{Despeyroux97}
J.~Despeyroux, F.~Pfenning, and C.~Sch{\"u}rmann.
\newblock Primitive recursion for higher-order abstract syntax.
\newblock In R.~Hindley, editor, {\em Proceedings of the Third International
  Conference on Typed Lambda Calculus and Applications (TLCA'97)}, pages
  147--163, Nancy, France, Apr. 1997. Springer-Verlag LNCS.

\bibitem{Hanus96RTA}
M.~Hanus and C.~Prehofer.
\newblock Higher-order narrowing with definitional trees.
\newblock In {\em Proc.\ Seventh International Conference on Rewriting
  Techniques and Applications (RTA'96)}, pages 138--152. Springer LNCS 1103,
  1996.

\bibitem{Kunen87}
K.~Kunen.
\newblock Answer sets and negation-as-failure.
\newblock In J.-L. Lassez, editor, {\em Proceedings of the Fourth International
  Conference on Logic Programming ({ICLP} '87)}, pages 219--228, Melbourne,
  Australia, May 1987. MIT Press.

\bibitem{Lassez87}
J.-L. Lassez and K.~Marriot.
\newblock Explicit representation of terms defined by counter examples.
\newblock {\em Journal of Automated Reasoning}, 3(3):301--318, Sept. 1987.

\bibitem{Lug95}
D.~Lugiez.
\newblock Positive and negative results for higher-order disunification.
\newblock {\em Journal of Symbolic Computation}, 20(4):431--470, Oct. 1995.

\bibitem{Michaylov91}
S.~Michaylov and F.~Pfenning.
\newblock Natural semantics and some of its meta-theory in {Elf}.
\newblock In L.-H. Eriksson, L.~Halln{\"a}s, and P.~Schroeder-Heister, editors,
  {\em Proceedings of the Second International Workshop on Extensions of Logic
  Programming}, pages 299--344, Stockholm, Sweden, Jan. 1991. Springer-Verlag
  LNAI 596.

\bibitem{Miller91jlc}
D.~Miller.
\newblock A logic programming language with lambda-abstraction, function
  variables, and simple unification.
\newblock {\em Journal of Logic and Computation}, 1(4):497--536, 1991.

\bibitem{Momigliano99phd}
A.~Momigliano.
\newblock {\em Elimination of negation in a logical framework}.
\newblock PhD thesis, Carnegie Mellon University, Forthcoming.

\bibitem{Nipkow91lics}
T.~Nipkow.
\newblock Higher-order critical pairs.
\newblock In G.~Kahn, editor, {\em Sixth Annual {IEEE} Symposium on Logic in
  Computer Science}, pages 342--349, Amsterdam, The Netherlands, July 1991.

\bibitem{Pfenning91lf}
F.~Pfenning.
\newblock Logic programming in the {LF} logical framework.
\newblock In G.~Huet and G.~Plotkin, editors, {\em Logical Frameworks}, pages
  149--181. Cambridge University Press, 1991.

\bibitem{Pfenning91lics}
F.~Pfenning.
\newblock Unification and anti-unification in the {Calculus} of
  {Constructions}.
\newblock In {\em Sixth Annual {IEEE} Symposium on Logic in Computer Science},
  pages 74--85, Amsterdam, The Netherlands, July 1991.

\bibitem{Schurmann98cade}
C.~Sch{\"u}rmann and F.~Pfenning.
\newblock Automated theorem proving in a simple meta-logic for {LF}.
\newblock In C.~Kirchner and H.~Kirchner, editors, {\em Proceedings of the 15th
  International Conference on Automated Deduction (CADE-15)}, pages 286--300,
  Lindau, Germany, July 1998. Springer-Verlag LNCS 1421.

\bibitem{Wright92}
D.~A. Wright.
\newblock {\em Reduction types and intensionality in the lambda-calculus}.
\newblock PhD thesis, University of Tasmania, Sept. 1992.

\end{thebibliography}
