\providecommand{\bysame}{\leavevmode\hbox to3em{\hrulefill}\thinspace}
\providecommand{\MR}{\relax\ifhmode\unskip\space\fi MR }
% \MRhref is called by the amsart/book/proc definition of \MR.
\providecommand{\MRhref}[2]{%
  \href{http://www.ams.org/mathscinet-getitem?mr=#1}{#2}
}
\providecommand{\href}[2]{#2}
\begin{thebibliography}{10}

\bibitem{AehligSchwichtenberg00}
Klaus Aehlig and Helmut Schwichtenberg, \emph{A syntactical analysis of
  non-size-increa\-sing polynomial time computation}, Proceedings 15'th
  Symposium on Logic in Computer Science (LICS 2000), 2000, pp.~84--91.

\bibitem{Berger93a}
Ulrich Berger, \emph{Program extraction from normalization proofs}, Typed
  Lambda Calculi and Applications (M.~Bezem and J.F. Groote, eds.), LNCS, vol.
  664, Springer Verlag, Berlin, Heidelberg, New York, 1993, pp.~91--106.

\bibitem{BergerBuchholzSchwichtenberg02}
Ulrich Berger, Wilfried Buchholz, and Helmut Schwichtenberg, \emph{Refined
  program extraction from classical proofs}, Annals of Pure and Applied Logic
  \textbf{114} (2002), 3--25.

\bibitem{BergerEberlSchwichtenberg03}
Ulrich Berger, Matthias Eberl, and Helmut Schwichtenberg, \emph{Term rewriting
  for normalization by evaluation}, Information and Computation \textbf{183}
  (2003), 19--42.

\bibitem{BergerSchwichtenberg91a}
Ulrich Berger and Helmut Schwichtenberg, \emph{An inverse of the evaluation
  functional for typed $\lambda$-calculus}, Proceedings 6'th Symposium on Logic
  in Computer Science (LICS'91) (R.~Vemuri, ed.), IEEE Computer Society Press,
  Los Alamitos, 1991, pp.~203--211.

\bibitem{Berghofer03}
Stefan Berghofer, \emph{Proofs, programs and executable specifications in
  higher order logic}, Ph.D. thesis, Institut f\"ur Informatik, TU M\"unchen,
  2003.

\bibitem{Hofmann99}
Martin Hofmann, \emph{Linear types and non-size-increasing polynomial time
  computation}, Proceedings 14'th Symposium on Logic in Computer Science
  (LICS'99), 1999, pp.~464--473.

\bibitem{JoachimskiMatthes03}
Felix Joachimski and Ralph Matthes, \emph{{Short proofs of normalisation for
  the simply-typed $\lambda$-calculus, permutative conversions and G{\"o}del's
  $T$}}, Archive for Mathematical Logic \textbf{42} (2003), 59--87.

\bibitem{Matthes98}
Ralph Matthes, \emph{{Extensions of System $F$ by Iteration and Primitive
  Recursion on Monotone Inductive Types}}, Ph.D. thesis, Ma\-the\-ma\-ti\-sches
  Institut der Universit{\"a}t M{\"u}nchen, 1998.

\bibitem{Miller91b}
Dale Miller, \emph{A logic programming language with lambda--abstraction,
  function variables and simple unification}, Journal of Logic and Computation
  \textbf{2} (1991), no.~4, 497--536.

\bibitem{Nipkow91}
Tobias Nipkow, \emph{Higher-order critical pairs}, Proceedings of the Sixth
  Annual IEEE Symposium on Logic in Computer Science (Los Alamitos) (R.~Vemuri,
  ed.), IEEE Computer Society Press, 1991, pp.~342--349.

\bibitem{Stoltenberg94}
Viggo Stoltenberg-Hansen, Edward Griffor, and Ingrid Lindstr{\"o}m,
  \emph{Mathematical theory of domains}, Cambridge Tracts in Theoretical
  Computer Science, Cambridge University Press, 1994.

\bibitem{TroelstraSchwichtenberg00}
Anne~S. Troelstra and Helmut Schwichtenberg, \emph{Basic proof theory}, 2nd
  ed., Cambridge University Press, 2000.

\end{thebibliography}
