\begin{thebibliography}{}

\bibitem[Abramsky and Jung, 1994]{abramsky:jung}
Abramsky, S. and Jung, A. (1994).
\newblock Domain theory.
\newblock In Abramsky, S., Gabbay, D., and Maibaum, T., editors, {\em Handbook
  of Logic in Computer Science}, volume~3 of {\em Oxford science publications},
  pages 1--168. Oxford university press.

\bibitem[Avigad and Feferman, 1998]{Avigad(98)}
Avigad, J. and Feferman, S. (1998).
\newblock G\"odel's functional (``{D}ialectica") interpretation.
\newblock In Buss, S.~R., editor, {\em Handbook of proof theory}, volume 137 of
  {\em Studies in Logic and the Foundations of Mathematics}, pages 337--405.
  North Holland, Amsterdam.

\bibitem[Battenfeld et~al., 2006]{simpson:compactly:generated}
Battenfeld, I., Schr{\"o}der, M., and Simpson, A. (2006).
\newblock Compactly generated domain theory.
\newblock {\em Math. Structures Comput. Sci.}, 16(2):141--161.

\bibitem[Battenfeld et~al., 2007]{simpson:convenient}
Battenfeld, I., Schr{\"o}der, M., and Simpson, A. (2007).
\newblock A convenient category of domains.
\newblock In {\em Computation, meaning, and logic: articles dedicated to Gordon
  Plotkin}, volume 172 of {\em Electron. Notes Theor. Comput. Sci.}, pages
  69--99. Elsevier, Amsterdam.

\bibitem[Bauer, 2002]{bauer:relationship}
Bauer, A. (2002).
\newblock A relationship between equilogical spaces and type two effectivity.
\newblock {\em MLQ Math. Log. Q.}, 48(suppl. 1):1--15.

\bibitem[Beki{\v{c}}, 1984]{bekic}
Beki{\v{c}}, H. (1984).
\newblock {\em Programming languages and their definition}, volume 177 of {\em
  Lecture Notes in Computer Science}.
\newblock Springer-Verlag, Berlin.
\newblock Selected papers edited by C. B. Jones.

\bibitem[Berardi et~al., 1998]{Berardi(98)}
Berardi, S., Bezem, M., and Coquand, T. (1998).
\newblock On the computational content of the axiom of choice.
\newblock {\em The Journal of Symbolic Logic}, 63(2):600--622.

\bibitem[Berger and Oliva, 2005]{BO(02A)}
Berger, U. and Oliva, P. (2005).
\newblock Modified bar recursion and classical dependent choice.
\newblock {\em Lect. Notes Log.}, 20:89--107.

\bibitem[Berger and Oliva, 2006]{berger:oliva:mbr}
Berger, U. and Oliva, P. (2006).
\newblock Modified bar recursion.
\newblock {\em Math. Structures Comput. Sci.}, 16(2):163--183.

\bibitem[Bezem, 1985]{Bezem(85)}
Bezem, M. (1985).
\newblock Strongly majorizable functionals of finite type: a model for bar
  recursion containing discontinuous functionals.
\newblock {\em The Journal of Symbolic Logic}, 50:652--660.

\bibitem[Bove and Dybjer, 2008]{bove:dybjer}
Bove, A. and Dybjer, P. (2008).
\newblock Dependent types at work.
\newblock Lecture notes from the LerNET Summer School, Piriapolis, available at
  the authors' web pages.

\bibitem[Escard\'o, 2007]{escardo:lics07}
Escard\'o, M. (2007).
\newblock Infinite sets that admit fast exhaustive search.
\newblock In {\em Proceedings of the 22nd Annual IEEE Symposium on Logic In
  Computer Science}, pages 443--452. IEEE Computer Society.

\bibitem[Escard{\'o}, 2008]{escardo:exhaustible}
Escard{\'o}, M. (2008).
\newblock Exhaustible sets in higher-type computation.
\newblock {\em Log. Methods Comput. Sci.}, 4(3):3:3, 37.

\bibitem[Escard{\'o} et~al., 2004]{escardo:lawson:simpson}
Escard{\'o}, M., Lawson, J., and Simpson, A. (2004).
\newblock Comparing {C}artesian closed categories of (core) compactly generated
  spaces.
\newblock {\em Topology Appl.}, 143(1-3):105--145.

\bibitem[Hutton, 2007]{haskell:hutton}
Hutton, G. (2007).
\newblock {\em {Programming in Haskell}}.
\newblock Cambridge University Press.

\bibitem[Johnstone, 2002]{johnstone:elephant}
Johnstone, P. (2002).
\newblock {\em Sketches of an Elephant: a Topos Theory Compendium}.
\newblock Oxford University Press.

\bibitem[Kock, 1970a]{kock:strong}
Kock, A. (1970a).
\newblock Monads on symmetric monoidal closed categories.
\newblock {\em Arch. Math. (Basel)}, 21:1--10.

\bibitem[Kock, 1970b]{kock:double}
Kock, A. (1970b).
\newblock On double dualization monads.
\newblock {\em Math. Scand.}, 27:151--165 (1971).

\bibitem[Kock, 1972]{kock:monoidal}
Kock, A. (1972).
\newblock Strong functors and monoidal monads.
\newblock {\em Arch. Math. (Basel)}, 23:113--120.

\bibitem[Lambek and Scott, 1986]{lambek:scott}
Lambek, J. and Scott, P. (1986).
\newblock {\em Introduction to Higher Order Categorical Logic}.
\newblock Cambridge University Press.

\bibitem[Mac~Lane, 1971]{maclane}
Mac~Lane, S. (1971).
\newblock {\em Categories for the Working Mathematician}.
\newblock Springer.

\bibitem[Moggi, 1990]{moggi:abstract}
Moggi, E. (1990).
\newblock An abstract view of programming languages.
\newblock Technical Report ECS-LFCS-90-113, Laboratory for Foundations of
  Computer Science, University of Edinburgh.

\bibitem[Moggi, 1991]{moggi:monads}
Moggi, E. (1991).
\newblock Notions of computation and monads.
\newblock {\em Information and Computation}, 93(1):55--92.

\bibitem[Nisan et~al., 2007]{Nisan(2007)}
Nisan, N. et~al. (2007).
\newblock {\em Algorithmic Game Theory}.
\newblock Cambridge University Press.

\bibitem[Normann, 1980]{normann:recursion}
Normann, D. (1980).
\newblock {\em Recursion on the countable functionals}, volume 811 of {\em Lec.
  Not. Math.}
\newblock Springer.

\bibitem[Normann, 1999]{Normann(99)}
Normann, D. (1999).
\newblock The continuous functionals.
\newblock In Griffor, E.~R., editor, {\em Handbook of Computability Theory},
  chapter~8, pages 251--275. North Holland, Amsterdam.

\bibitem[Oliva, 2006]{oliva:understanding}
Oliva, P. (2006).
\newblock {Understanding and using Spector's bar recursive interpretation of
  classical analysis.}
\newblock {Beckmann, Arnold (ed.) et al., Logical approaches to computational
  barriers. Second conference on computability in Europe, CiE 2006, Swansea,
  UK, June 30--July 5, 2006. Proceedings. Berlin: Springer. Lecture Notes in
  Computer Science 3988, 423-434 (2006).}

\bibitem[Schr{\"o}der, 2002]{schroeder:extended}
Schr{\"o}der, M. (2002).
\newblock Extended admissibility.
\newblock {\em Theoret. Comput. Sci.}, 284(2):519--538.

\bibitem[Smyth, 1977]{smyth:effectively}
Smyth, M. (1977).
\newblock Effectively given domains.
\newblock {\em Theoret. Comput. Sci.}, 5(1):256--274.

\bibitem[Spector, 1962]{Spector(62)}
Spector, C. (1962).
\newblock Provably recursive functionals of analysis: a consistency proof of
  analysis by an extension of principles in current intuitionistic mathematics.
\newblock In Dekker, F. D.~E., editor, {\em Recursive Function Theory: Proc.
  Symposia in Pure Mathematics}, volume~5, pages 1--27. American Mathematical
  Society, Providence, Rhode Island.

\bibitem[Valiente, 2002]{Valiente(2002)}
Valiente, G. (2002).
\newblock {\em Algorithms on Trees and Graphs}.
\newblock Springer.

\end{thebibliography}