[1]    Klaus Aehlig and Helmut Schwichtenberg, A syntactical analysis of non-size-increasing polynomial time computation, Proceedings 15’th Symposium on Logic in Computer Science (LICS 2000), 2000, pp. 84–91.

[2]    Ulrich Berger, 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.

[3]    Ulrich Berger, Wilfried Buchholz, and Helmut Schwichtenberg, Refined program extraction from classical proofs, Annals of Pure and Applied Logic 114 (2002), 3–25.

[4]    Ulrich Berger, Matthias Eberl, and Helmut Schwichtenberg, Term rewriting for normalization by evaluation, Information and Computation 183 (2003), 19–42.

[5]    Ulrich Berger and Helmut Schwichtenberg, An inverse of the evaluation functional for typed λ-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.

[6]    Stefan Berghofer, Proofs, programs and executable specifications in higher order logic, Ph.D. thesis, Institut für Informatik, TU München, 2003.

[7]    Martin Hofmann, Linear types and non-size-increasing polynomial time computation, Proceedings 14’th Symposium on Logic in Computer Science (LICS’99), 1999, pp. 464–473.

[8]    Felix Joachimski and Ralph Matthes, Short proofs of normalisation for the simply-typed λ-calculus, permutative conversions and Gödel’s T, Archive for Mathematical Logic 42 (2003), 59–87.

[9]    Ralph Matthes, Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types, Ph.D. thesis, Mathematisches Institut der Universität München, 1998.

[10]    Dale Miller, A logic programming language with lambda–abstraction, function variables and simple unification, Journal of Logic and Computation 2 (1991), no. 4, 497–536.

[11]    Tobias Nipkow, 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.

[12]    Viggo Stoltenberg-Hansen, Edward Griffor, and Ingrid Lindström, Mathematical theory of domains, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1994.

[13]    Anne S. Troelstra and Helmut Schwichtenberg, Basic proof theory, 2nd ed., Cambridge University Press, 2000.