1: \begin{thebibliography}{}
2:
3: \bibitem[\protect\citeauthoryear{Anderson and Belnap}{Anderson and
4: Belnap}{1975}]{Anderson75}
5: {\sc Anderson, A.} {\sc and} {\sc Belnap, N.} 1975.
6: \newblock {\em Entailment. The Logic of Relevance and Necessity}. Vol.~1.
7: \newblock Princeton University Press.
8:
9: \bibitem[\protect\citeauthoryear{Baker-Finch}{Baker-Finch}{1993}]{Baker94}
10: {\sc Baker-Finch, C.~A.} 1993.
11: \newblock Relevance and contraction: A logical basis for strictness and sharing
12: analysis.
13: \newblock Tech. Rep. ISE RR 34/94, University of Canberra.
14:
15: \bibitem[\protect\citeauthoryear{Barbuti, Mancarella, Pedreschi, and
16: Turini}{Barbuti et~al\mbox{.}}{1990}]{Bar90}
17: {\sc Barbuti, R.}, {\sc Mancarella, P.}, {\sc Pedreschi, D.}, {\sc and} {\sc
18: Turini, F.} 1990.
19: \newblock {A} transformational approach to negation in logic programming.
20: \newblock {\em Journal of Logic Programming\/}~{\em 8}, 201--228.
21:
22: \bibitem[\protect\citeauthoryear{Belnap}{Belnap}{1974}]{Belnap74}
23: {\sc Belnap, N.} 1974.
24: \newblock Functions which really depend on their argument.
25: \newblock Manuscript.
26:
27: \bibitem[\protect\citeauthoryear{Belnap}{Belnap}{1993}]{Belnap93}
28: {\sc Belnap, N.~D.} 1993.
29: \newblock Life in the undistributed middle.
30: \newblock In {\em Substructural Logics}, {K.~Do{\v{s}}en} {and}
31: {P.~Schroeder-Heister}, Eds. Oxford University Press, 31--42.
32:
33: \bibitem[\protect\citeauthoryear{Church}{Church}{1941}]{Church41}
34: {\sc Church, A.} 1941.
35: \newblock {\em The Calculi of Lambda Conversion}.
36: \newblock Princeton University Press.
37:
38: \bibitem[\protect\citeauthoryear{Church}{Church}{1951}]{Church51}
39: {\sc Church, A.} 1951.
40: \newblock The weak theory of implication.
41: \newblock In {\em Kontrolliertes Denken}, {A.Menne}, {A.~Wilhelmy}, {and}
42: {H.~Angsil}, Eds. Kommissions-Verlag Karl Alber, Munich, 22--27.
43:
44: \bibitem[\protect\citeauthoryear{Comon}{Comon}{1991}]{Comon91}
45: {\sc Comon, H.} 1991.
46: \newblock Disunification: a survey.
47: \newblock In {\em Computational Logic: Essays in Honor of Alan Robinson},
48: {J.-L. Lassez} {and} {G.Plotkin}, Eds. MIT Press, Cambridge, MA, 322--359.
49:
50: \bibitem[\protect\citeauthoryear{Despeyroux, Pfenning, and
51: Sch{\"u}rmann}{Despeyroux et~al\mbox{.}}{1997}]{Despeyroux97}
52: {\sc Despeyroux, J.}, {\sc Pfenning, F.}, {\sc and} {\sc Sch{\"u}rmann, C.}
53: 1997.
54: \newblock Primitive recursion for higher-order abstract syntax.
55: \newblock In {\em Proceedings of the Third International Conference on Typed
56: Lambda Calculus and Applications (TLCA'97)}, {R.~Hindley}, Ed.
57: Springer-Verlag LNCS, Nancy, France, 147--163.
58: \newblock An extended version is available as Technical Report CMU-CS-96-172,
59: Carnegie Mellon University.
60:
61: \bibitem[\protect\citeauthoryear{Ghani, Paiva, and Ritter}{Ghani
62: et~al\mbox{.}}{1998}]{Ghani98}
63: {\sc Ghani, N.}, {\sc Paiva, V.~D.}, {\sc and} {\sc Ritter, E.} 1998.
64: \newblock Linear explicit substitutions.
65: \newblock Tech. Rep. CSR-98-2, University of Birmingham, School of Computer
66: Science. Mar.
67:
68: \bibitem[\protect\citeauthoryear{Hanus and Prehofer}{Hanus and
69: Prehofer}{1996}]{Hanus96RTA}
70: {\sc Hanus, M.} {\sc and} {\sc Prehofer, C.} 1996.
71: \newblock Higher-order narrowing with definitional trees.
72: \newblock In {\em Proc.\ Seventh International Conference on Rewriting
73: Techniques and Applications (RTA'96)}. Springer LNCS 1103, 138--152.
74:
75: \bibitem[\protect\citeauthoryear{Helmann}{Helmann}{1977}]{Helman77}
76: {\sc Helmann, G.} 1977.
77: \newblock Completeness of the normal typed fragment of the $\lambda$-system
78: $u$.
79: \newblock {\em Journal of Philosophical Logic\/}~{\em 6,\/}~2, 33--46.
80:
81: \bibitem[\protect\citeauthoryear{Jensen}{Jensen}{1991}]{Jensen91}
82: {\sc Jensen, T.~P.} 1991.
83: \newblock {Strictness Analysis in Logical Form}.
84: \newblock In {\em {Functional Programming Languages and Computer
85: Architectures}}, {J.~Hughes}, Ed. Lecture Notes in Computer Science, vol.
86: 523. Springer, Berlin, Harvard, Massachusetts, USA, 352--366.
87:
88: \bibitem[\protect\citeauthoryear{Kunen}{Kunen}{1987}]{Kunen87}
89: {\sc Kunen, K.} 1987.
90: \newblock Answer sets and negation-as-failure.
91: \newblock In {\em Proceedings of the Fourth International Conference on Logic
92: Programming ({ICLP} '87)}, {J.-L. Lassez}, Ed. MIT Press, Melbourne,
93: Australia, 219--228.
94:
95: \bibitem[\protect\citeauthoryear{Lassez, Maher, and Marriot}{Lassez
96: et~al\mbox{.}}{1988}]{Lassez88}
97: {\sc Lassez, J.-L.}, {\sc Maher, M.}, {\sc and} {\sc Marriot, K.} 1988.
98: \newblock Unification revisited.
99: \newblock In {\em Foundations of Deductive Databases and Logic Programming},
100: {J.~Minker}, Ed. Morgan Kaufmann, Los Altos,CA.
101:
102: \bibitem[\protect\citeauthoryear{Lassez and Marriot}{Lassez and
103: Marriot}{1987}]{Lassez87}
104: {\sc Lassez, J.-L.} {\sc and} {\sc Marriot, K.} 1987.
105: \newblock Explicit representation of terms defined by counter examples.
106: \newblock {\em Journal of Automated Reasoning\/}~{\em 3,\/}~3 (Sept.),
107: 301--318.
108:
109: \bibitem[\protect\citeauthoryear{Lugiez}{Lugiez}{1995}]{Lug95}
110: {\sc Lugiez, D.} 1995.
111: \newblock Positive and negative results for higher-order disunification.
112: \newblock {\em Journal of Symbolic Computation\/}~{\em 20,\/}~4 (Oct.),
113: 431--470.
114:
115: \bibitem[\protect\citeauthoryear{Miller}{Miller}{1991}]{Miller91jlc}
116: {\sc Miller, D.} 1991.
117: \newblock A logic programming language with lambda-abstraction, function
118: variables, and simple unification.
119: \newblock {\em Journal of Logic and Computation\/}~{\em 1,\/}~4, 497--536.
120:
121: \bibitem[\protect\citeauthoryear{Momigliano}{Momigliano}{2000a}]{Momigliano00p%
122: hd}
123: {\sc Momigliano, A.} 2000a.
124: \newblock Elimination of negation in a logical framework.
125: \newblock Ph.D. thesis, Department of Philosophy, Carnegie Mellon University.
126: \newblock Available as Technical Report CMU-CS-00-175.
127:
128: \bibitem[\protect\citeauthoryear{Momigliano}{Momigliano}{2000b}]{Momigliano00c%
129: sl}
130: {\sc Momigliano, A.} 2000b.
131: \newblock Elimination of negation in a logical framework.
132: \newblock In {\em Proceedings of the 14th Annual Conference of the European
133: Association for Computer Science Logic (CSL'00)}, {P.~G. Clote} {and}
134: {H.~Schwichtenberg}, Eds. Springer-Verlag LNCS, Fischbachau, Germany,
135: 411--426.
136:
137: \bibitem[\protect\citeauthoryear{Mycroft}{Mycroft}{1980}]{Mycroft80}
138: {\sc Mycroft, A.} 1980.
139: \newblock The theory and practice of transforming call-by-need to
140: call-by-value.
141: \newblock In {\em Proceedings of the 4th International Symposium on
142: Programming}. Lecture Notes in Computer Science, vol.~83. Springer Verlag,
143: 269--281.
144:
145: \bibitem[\protect\citeauthoryear{Nipkow}{Nipkow}{1991}]{Nipkow91lics}
146: {\sc Nipkow, T.} 1991.
147: \newblock Higher-order critical pairs.
148: \newblock In {\em Sixth Annual {IEEE} Symposium on Logic in Computer Science},
149: {G.~Kahn}, Ed. Amsterdam, The Netherlands, 342--349.
150:
151: \bibitem[\protect\citeauthoryear{Nipkow}{Nipkow}{1993}]{Nipkow93tlca}
152: {\sc Nipkow, T.} 1993.
153: \newblock Orthogonal higher-order rewrite systems are confluent.
154: \newblock In {\em Proceedings of the International Conference on Typed Lambda
155: Calculi and Applications}, {M.~Bezem} {and} {J.~Groote}, Eds. Utrecht, The
156: Netherlands, 306--317.
157:
158: \bibitem[\protect\citeauthoryear{Pfenning}{Pfenning}{1991a}]{Pfenning91lf}
159: {\sc Pfenning, F.} 1991a.
160: \newblock Logic programming in the {LF} logical framework.
161: \newblock In {\em Logical Frameworks}, {G.~Huet} {and} {G.~Plotkin}, Eds.
162: Cambridge University Press, 149--181.
163:
164: \bibitem[\protect\citeauthoryear{Pfenning}{Pfenning}{1991b}]{Pfenning91lics}
165: {\sc Pfenning, F.} 1991b.
166: \newblock Unification and anti-unification in the {Calculus} of
167: {Constructions}.
168: \newblock In {\em Sixth Annual {IEEE} Symposium on Logic in Computer Science}.
169: Amsterdam, The Netherlands, 74--85.
170:
171: \bibitem[\protect\citeauthoryear{Pfenning}{Pfenning}{2000}]{Pfenning00saig}
172: {\sc Pfenning, F.} 2000.
173: \newblock Reasoning about staged computation.
174: \newblock In {\em Proceedings of the International Workshop on Semantics,
175: Applications, and Implementation of Program Generation (SAIG 2000)},
176: {W.~Taha}, Ed. Springer-Verlag LNCS 1924, Montreal, Canada, 5--6.
177: \newblock Abstract of invited talk.
178:
179: \bibitem[\protect\citeauthoryear{Pfenning}{Pfenning}{2001a}]{Pfenning01book}
180: {\sc Pfenning, F.} 2001a.
181: \newblock {\em Computation and Deduction}.
182: \newblock Cambridge University Press.
183: \newblock In preparation. Draft from April 1997 available electronically.
184:
185: \bibitem[\protect\citeauthoryear{Pfenning}{Pfenning}{2001b}]{Pfenning01lics}
186: {\sc Pfenning, F.} 2001b.
187: \newblock Intensionality, extensionality, and proof irrelevance in modal type
188: theory.
189: \newblock In {\em Proceedings of the 16th Annual Symposium on Logic in Computer
190: Science (LICS'01)}, {J.~Halpern}, Ed. IEEE Computer Society Press, Boston,
191: Massachusetts, 221--230.
192: \newblock Extended version available as Technical Report CMU-CS-01-116,
193: Department of Computer Science, Carnegie Mellon University, September 2001.
194:
195: \bibitem[\protect\citeauthoryear{Sch{\"u}rmann and Pfenning}{Sch{\"u}rmann and
196: Pfenning}{1998}]{Schurmann98cade}
197: {\sc Sch{\"u}rmann, C.} {\sc and} {\sc Pfenning, F.} 1998.
198: \newblock Automated theorem proving in a simple meta-logic for {LF}.
199: \newblock In {\em Proceedings of the 15th International Conference on Automated
200: Deduction (CADE-15)}, {C.~Kirchner} {and} {H.~Kirchner}, Eds. Springer-Verlag
201: LNCS 1421, Lindau, Germany, 286--300.
202:
203: \bibitem[\protect\citeauthoryear{Tsung-Min and Mishra}{Tsung-Min and
204: Mishra}{1989}]{Kuo89}
205: {\sc Tsung-Min, K.} {\sc and} {\sc Mishra, P.} 1989.
206: \newblock {Strictness Analysis: A New Perspective Based on Type Inference}.
207: \newblock In {\em {FPCA '89, Functional Programming Languages and Computer
208: Architecture}}. ACM Press, New York, London, UK, September 11--13.
209:
210: \bibitem[\protect\citeauthoryear{Wright}{Wright}{1992}]{Wright92}
211: {\sc Wright, D.~A.} 1992.
212: \newblock Reduction types and intensionality in the lambda-calculus.
213: \newblock Ph.D. thesis, University of Tasmania.
214:
215: \bibitem[\protect\citeauthoryear{Wright}{Wright}{1996}]{Wright96}
216: {\sc Wright, D.~A.} 1996.
217: \newblock Linear, strictness and usage logics.
218: \newblock In {\em Proceedings of Conference on Computing: The Australian Theory
219: Symposium}, {M.~E. Houle} {and} {P.~Eades}, Eds. Australian Computer Science
220: Communications, Townsville, 73--80.
221:
222: \end{thebibliography}
223: