\begin{thebibliography}{10}

\bibitem{anderson-belnap}
Allan~Ross Anderson and Nuel~D.\ Belnap.
\newblock {\em Entailment: the Logic of Relevance and Necessity, volume I}.
\newblock Princeton University Press, Princeton NJ, 1975.

\bibitem{beth:foundations-of-mathematics}
E.\~W.\ Beth.
\newblock {\em The Foundations of Mathematics, A Study in the Philosophy of
  Science}.
\newblock Studies in Logic and the Foundations of Mathematics. North-Holland
  Publishing Company, Amsterdam, 1959.

\bibitem{curry-feys:combinatory-logic}
H.~B. Curry and R.~Feys.
\newblock {\em Combinatory Logic Volume {I}}.
\newblock Studies in Logic and the Foundations of Mathematics. North-Holland
  Publishing Company, Amsterdam, 1958.

\bibitem{dummett:intuitionism}
M.~A.~E. Dummett.
\newblock {\em Elements of Intuitionism}.
\newblock Oxford University Press, 1977.

\bibitem{fitting:intuitionistic-logic}
M.~C. Fitting.
\newblock {\em Intuitionistic Logic, Model Theory, and Forcing}.
\newblock Studies in Logic and the Foundations of Mathematics. North-Holland
  Publishing Company, Amsterdam, London, 1969.

\bibitem{GirardLT}
J.-Y. Girard, Y.~Lafont, and P.~Taylor.
\newblock {\em Proofs and Types}.
\newblock Cambridge Tracts in Theoretical Computer Science. Cambridge
  University Press, 1989.

\bibitem{grayson}
R.\ Grayson.
\newblock Forcing in intuitionistic set theory without power set.
\newblock {\em Journal of Symbolic Logic}, 48:670--682, 1983.

\bibitem{heyting:regeln-intuitionistischen-logik}
A.~Heyting.
\newblock Die formalen {Regeln} der intuitionistischen {Logik}.
\newblock {\em Sitzungsberichte der Preussischen Academie der Wissenschaften,
  Physikalisch-Matematische Klasse}, pages 42--56, 1930.

\bibitem{howard:formulae-as-types}
W.~A. Howard.
\newblock The formulae-as-types notion of construction.
\newblock In J.~P. Seldin and J.~R. Hindley, editors, {\em To {H.~B.~Curry}:
  Essays on Combinatory Logic, Lambda Calculus and Formalism}, pages 479--490.
  Academic Press, 1980.

\bibitem{kleene:intuitionistic-number-theory}
S.~C. Kleene.
\newblock On the interpretation of intuitionistic number theory.
\newblock {\em The Journal of Symbolic Logic}, 10(4):109--124, December 1945.

\bibitem{kleene:realizability-59}
S.~C. Kleene.
\newblock Realizability.
\newblock In A.~Heyting, editor, {\em Constructivity in Mathematics}, pages
  285--289. North-Holland Publishing Company, Amsterdam, 1959.
\newblock Proceedings of the Colloquium Held in Amsterdam, August 26--31, 1957.

\bibitem{kleene-vesley:foundations}
S.~C. Kleene and R.~E. Vesley.
\newblock {\em The Foundations of Intuitionistic Mathematics, Especially in
  Relation to Recursive Functions}.
\newblock Studies in Logic and the Foundations of Mathematics. North-Holland
  Publishing Company, Amsterdam, London, 1965.

\bibitem{kripke:modal-semantics-I}
S.~A. Kripke.
\newblock Semantical analysis of modal logic {I}: Normal modal propositional
  calculi.
\newblock {\em Zeitschrift f{\"u}r Mathematische Logik und Grundlagen der
  Mathematik}, 9:67--96, 1963.

\bibitem{kripke:semantics-of-intuitionism}
S.~A. Kripke.
\newblock Semantical analysis of intuitionistic logic, {I}.
\newblock In J.~N. Crossley and M.~A.~E. Dummett, editors, {\em Formal Systems
  and Recursive Functions}, pages 92--130. North-Holland Publishing Company,
  Amsterdam, 1965.
\newblock Proceedings of the Eighth Logic Colloquium, Oxford, July 1963.

\bibitem{KMO}
Stuart~A.\ Kurtz, John~C.\ Mitchell, and Michael~J.\ O'Donnell.
\newblock Connecting formal semantics to constructive intuitions.
\newblock In J.\~P.\ Myers and M.\~J.\ O'Donnell, editors, {\em Constructivity
  in Computer Science}, volume 613 of {\em Lecture Notes in Computer Science},
  pages 1--21, Berlin, 1992. Springer-Verlag.
\newblock Proceedings of the Summer Symposium, San Antonio, TX, June 1991.

\bibitem{lauchli:realizability-70}
H.~L\"auchli.
\newblock An abstract notion of realizability for which intuitionistic
  predicate calculus is complete.
\newblock In A.~Kino, J.~Myhill, and R.~E. Vesley, editors, {\em Intuitionism
  and Proof Theory}, Studies in Logic and the Foundations of Mathematics, pages
  277--234. North-Holland Publishing Company, Amsterdam, London, 1970.
\newblock Proceedings of the Conference on Intuitionism and Proof Theory,
  Buffalo, New York, August 1968.

\bibitem{MitchTCS}
J.~C. Mitchell.
\newblock Type systems for programming languages.
\newblock In J.~van Leeuwen, editor, {\em Handbook of Theoretical Computer
  Science, Volume B}, pages 365--458. North-Holland, Amsterdam, 1990.

\bibitem{pitts}
Andrew~M.\ Pitts.
\newblock Poloymorphism is set-theoretic, constructively.
\newblock In D.\ Pitt, editor, {\em Proceedings of the Conference on Category
  Theory and Computer Science, Edinburgh, 1987}, volume 283 of {\em Lecture
  Notes in Computer Science}, pages 12--39, Berlin, 1987. Springer-Verlag.

\bibitem{prawitz}
D.~Prawitz.
\newblock {\em Natural Deduction}.
\newblock Almqvist \& Wiksell, Stockholm, 1965.

\bibitem{reynolds}
John~C.\ Reynolds.
\newblock {\em Polymorphism is Not Set-Theoretic}, volume 173 of {\em Lecture
  Notes in Computer Science}, pages 145--156.
\newblock Springer-Verlag, Berlin, 1984.

\bibitem{rose}
G.~F. Rose.
\newblock Propositional calculus and realizability.
\newblock {\em Transactions of the American Mathematical Society}, 75:1--19,
  July--September 1953.

\bibitem{StatRel}
R.~Statman.
\newblock Logical relations and the typed lambda calculus.
\newblock {\em Information and Control}, 65:85--97, 1985.

\bibitem{stenlund}
S\"oren Stenlund.
\newblock {\em Combinators, $\lambda$-terms, and Proof Theory}.
\newblock D. Riedel Publishing Company, Dordrecht-Holland, 1972.

\bibitem{tarski:classical-semantics}
Alfred Tarski.
\newblock Poj{\c e}cie prawdy w j{\c e}zykach nauk dedukcyjnch.
\newblock {\em Prace Towarzystwa Naukowego Warzawskiego}, 1933.
\newblock English translation in \cite{tarski:works}.

\bibitem{tarski:works}
Alfred Tarski.
\newblock {\em Logic, Semantics, and Metamathematics}.
\newblock Oxford University Press, 1956.

\bibitem{troelstra-van-dalen}
A.~S. Troelstra and D.~van Dalen.
\newblock {\em Constructivism in Mathematics: an Introduction}.
\newblock Studies in Logic and the Foundations of Mathematics. North-Holland,
  1988.

\bibitem{van-dalen}
D.\ {van Dalen}.
\newblock Intuitionistic logic.
\newblock In D.\ Gabbay and F.\ Guenther, editors, {\em Handbook of
  Philosophical Logic III}, pages 225--339. D.\ Reidel, Dordrecht, 1986.

\bibitem{wittgenstein:tractatus}
L.~Wittgenstein.
\newblock Tractatus logico-philo\-sophicus.
\newblock {\em Annalen der {Natur}-philo\-sophie}, 1921.
\newblock English translation in~\cite{wittgenstein:tractatus-english}.

\bibitem{wittgenstein:tractatus-english}
L.~Wittgenstein.
\newblock {\em Tractatus Logico-Philo\-sophicus}.
\newblock Routledge and Kegan Paul, 1961.

\end{thebibliography}