@string{north-holland = "North-Holland Publishing Company"}
@string{studies-in-logic="Studies in Logic and the Foundations of Mathematics"}
@string{jsl = "The Journal of Symbolic Logic"}
@string{zml="Zeitschrift f{\"u}r Mathematische Logik und Grundlagen der
		 Mathematik"}

@book{
        anderson-belnap,
        author = {Allan Ross Anderson and Nuel D.\ Belnap},
        title = {Entailment: the Logic of Relevance and Necessity,
		  volume I},
        publisher = {Princeton University Press},
        address = {Princeton NJ},
        year = {1975}
}

@book{
	beeson,
	author={M.\ J.\ Beeson},
	title={Foundations of Constructive Mathematics},
	publisher={Springer-Verlag},
	year={1980}
}

@book{
	beth:foundations-of-mathematics,
	author = {E.\ W.\ Beth},
	title = {The Foundations of Mathematics, A Study in the
		 Philosophy of Science},
	publisher = north-holland,
	year = {1959},
	series = studies-in-logic,
	address = {Amsterdam}
}

@article{
	BMM,
	author="K.\ B.\ Bruce and A.\ R.\ Meyer and J.\ C.\ Mitchell",
	title="The semantics of second-order lambda calculus",
	journal="Information and Computation",
	year="1990",Volume="85",Number="1",
	pages="76--134",
	note="Reprinted in
	{\it Logical Foundations of Functional Programming,}
	ed. G. Huet, Addison-Wesley (1990) 213--273."}

@article{	
	church:unsolvable-problem,
	author = {A. Church},
	title = {An Unsolvable Problem of Elementary Number Theory},
	journal = {American Journal of Mathematics},
	year = {1936},
	volume = {58},
	pages = {345--363}
}

@inproceedings{
	classical-satisfiability,
	author={S. A. Cook},
	title={The Complexity of Theorem-Proving Procedures},
	booktitle={3rd Annual ACM Symposium on Theory of Computing},
	year={1971},
	pages={151--158},
	organization={Association for Computing Machinery}
}

@book{
	curry-feys:combinatory-logic,
	author = {H. B. Curry and R. Feys},
	title = {Combinatory Logic Volume {I}},
	publisher = north-holland,
	year = {1958},
	series = studies-in-logic,
	address = {Amsterdam}
}

@article{
        deswart,
        author={H.\ C.\ M.\ {de Swart}},
        title={Another Intuitionistic Completeness Proof},
        journal={Journal of Symbolic Logic},
        volume={41},
        pages={644--662},
        year={1976}
}

@book{
	dummett:intuitionism,
	author={M. A. E. Dummett},
	title={Elements of Intuitionism},
	publisher={Oxford University Press},
	year={1977}
}

@article{
	dyckhoff,
	author={R. Dyckhoff},
	title={Contraction-Free Sequent Calculi for Intuitionistic Logic},
	journal={Journal of Symbolic Logic},
	year={1991},
	note={To appear}
}

@inproceedings{
	feferman:faithful-adequate,
	author={S. Feferman},
	title={Constructive Theories of Functions and Classes},
	booktitle={Logic Colloquium 78},
	year={1979},
	editor={M. Boffa and D. van Dalen and K. McAloon},
	pages={159--224},
	publisher={North-Holland},
	note={Proceedings of the colloquium held in Mons, August 1978}
}

@inproceedings{
	felleisen,
	author={M. Felleisen and D. Friedman and E. Kohlbecker and B. Duba},
	title={Reasoning with continuations},
	booktitle={Proceedings of the First Annual Symposium on Logic in
		Computer Science},
	pages={131--141},
	year={1986}
}

@book{
	fitting:intuitionistic-logic,
	author = {M. C. Fitting},
	title = {Intuitionistic Logic, Model Theory, and Forcing},
	publisher = north-holland,
	year = {1969},
	series = studies-in-logic,
	address = {Amsterdam, London}
}

@book{
	garey-johnson,
	author={M. R. Garey and D. S. Johnson},
	title={Computers and Intractability},
	publisher={W. H. Freeman},
	year={1979},
}

@article{
	gentzen,
	author={G. Gentzen},
	title={Beweisbarkeit und {Unbeweisbarkeit} von {Anfangsf\"allen}
	       der transfiniten {Induktion} in der reinen {Zahlentheorie}},
	journal={Mathematische Annalen},
	volume={119},
	pages={140--161},
	year={1943}
}

@incollection{
	girard:strong-normalization,
	author={Jean-Yves Girard},
	title={Une extension de l'interpr\'etation de {G\"odel} \`a
	       l'analysis, et son application \`a l'\'elimination des 
	       coupures dans l'analysis et la th\'eorie des types},
	booktitle={Proceedings 2nd Scandinavian Logic Symposium},
	editor={J. E. Fenstad},
	publisher={North-Holland},
	year={1971}
}

@book{
	GirardLT,
	author="J.-Y. Girard and Y. Lafont and P. Taylor",
	title="Proofs and Types",
	series="Cambridge Tracts in Theoretical
	Computer Science",
	publisher="Cambridge University Press",
	year="1989",pages="250"}

@article{
        grayson,
        author={R.\ Grayson},
        title={Forcing in Intuitionistic Set Theory Without Power
		  Set},
        journal={Journal of Symbolic Logic},
        year={1983},
        volume={48},
        pages={670--682}
}

@article{
	henkin:completeness,
	author={Leon Henkin},
	title={Completeness in the theory of types},
	journal=jsl,
	volume={15},
	pages={81--91},
	year={1950}
}

@article{
	heyting:regeln-intuitionistischen-logik,
	author = {A. Heyting},
	title  = {Die formalen {Regeln} der intuitionistischen {Logik}},
	journal= {Sitzungsberichte der Preussischen Academie der
		  Wissenschaften, Physikalisch-Matematische Klasse},
	year   = {1930},
	pages  = {42--56}
}

@book{
	heyting:intro,
	author={A. Heyting},
	title={Intuitionism, an introduction},
	publisher={North-Holland},
	year={1971}
}

@incollection{
	howard:formulae-as-types,
	author = {W. A. Howard},
	title = {The Formulae-As-Types Notion of Construction},
	booktitle = {To {H.~B.~Curry}: Essays on Combinatory Logic, 
		     Lambda Calculus and Formalism},
	publisher = {Academic Press},
	year = {1980},
	editor = {J. P. Seldin and J. R. Hindley},
	pages = {479--490}
}

@phdthesis{
	hudelmaier,
	author={J. Hudelmaier},
	title={Bounds for Cut Elimination in Intuitionistic Logic},
	school={Universit\"at T\"ubingen},
	year={1989}
}

@inproceedings{
	johnstone,
	author="P. T. Johnstone",
	title="Conditions Related to de {Morgan's} Law",
	booktitle="Applications of Sheaves.  Proceedings of the 

		   Research Symposium on Applications of Sheaf
		   Theory to Logic, Algebra, and Analysis",
	editor="M. P. Fourman and C. J. Mulvey and D. S. Scott",
	pages="479--491",
	year="1979",
	publisher="Springer Verlag",
	note="Lecture Notes in Mathematics 753"
}

@article{
	kleene:intuitionistic-number-theory,
	author = {S. C. Kleene},
	title = {On the Interpretation of Intuitionistic Number Theory},
	journal = jsl,
	year = {1945},
	volume = {10},
	number = {4},
	pages = {109--124},
	month = dec
}

@incollection{
	kleene:realizability-59,
	author = {S. C. Kleene},
	title = {Realizability},
	booktitle = {Constructivity in Mathematics},
	year = {1959},
	editor = {A. Heyting},
	pages = {285--289},
	publisher = north-holland,
	address = {Amsterdam},
	note = {Proceedings of the Colloquium Held in Amsterdam, 
		August 26--31, 1957}
}

@book{
	kleene:intro,
	author={S. C. Kleene},
	title={Introduction to Metamathematics},
	publisher={North-Holland},
	year={1971}
}

@book{
	kleene-vesley:foundations,
	author = {S. C. Kleene and R. E. Vesley},
	title = {The Foundations of Intuitionistic Mathematics,
		 Especially in Relation to Recursive Functions},
	publisher = north-holland,
	year = {1965},
	series = studies-in-logic,
	address = {Amsterdam, London}
}

@article{
	kreisel,
	author={Georg Kreisel},
	title={On Weak Completeness of Intuitionistic Logic},
	journal={Journal of Symbolic Logic},
	volume={27},
	page={139--158},
	year={1962}
}

@article{
	kripke:modal-semantics-I,
	author={S. A. Kripke},
	title={Semantical Analysis of Modal Logic {I}: Normal Modal
	       Propositional Calculi},
	journal=zml,
	volume={9},
	pages={67--96},
	year={1963}
}

@incollection{
	kripke:semantics-of-intuitionism,
	author = {S. A. Kripke},
	title = {Semantical Analysis of Intuitionistic Logic, {I}},
	booktitle = {Formal Systems and Recursive Functions},
	publisher = north-holland,
	year = {1965},
	editor = {J. N. Crossley and M. A. E. Dummett},
	pages = {92--130},
	address = {Amsterdam},
	note = {Proceedings of the Eighth Logic Colloquium, Oxford,
		July 1963}
}

@inproceedings{
        KMO,
        author = {Stuart A.\ Kurtz and John C.\ Mitchell and Michael
		  J.\ O'Donnell},
        title = {Connecting Formal Semantics to Constructive
		  Intuitions},
        booktitle = {Constructivity in Computer Science},
        editor = {J.\ P.\ Myers and M.\ J.\ O'Donnell},
        series = {Lecture Notes in Computer Science},
        volume = {613},
        publisher = {Springer-Verlag},
        address = {Berlin},
        year = {1992},
        pages = {1--21},
        note = {Proceedings of the Summer Symposium, San Antonio, TX,
		  June 1991}
}

@incollection{
	lauchli:realizability-70,
	author = {H. L\"auchli},
	label  = {L\"au70},
	title = {An Abstract Notion of Realizability for which
		 Intuitionistic Predicate Calculus is Complete},
	booktitle = {Intuitionism and Proof Theory},
        series = studies-in-logic,
	publisher = north-holland,
	address = {Amsterdam, London},
	year = {1970},
	editor = {A. Kino and J. Myhill and R. E. Vesley},
	pages = {277--234},
	note = {Proceedings of the Conference on Intuitionism and
		Proof Theory, Buffalo, New York, August 1968}
}

@article{
	leivant,
	author={D. M. E. Leivant},
	title={Failure of Completeness Properties for Intuitionistic
	       Predicate Logic for Constructive Models},
	journal={Annales Scientifiques de l'Universit\'e de Clermont-Ferrand
		 II, Section Mathematiques},
	volume={13},
	pages={93--107},
	year={1976}
}

@inproceedings{
	lincoln,
	author={P. Lincoln and A. Scedrov and N. Shankaar},
	title={Linearizing Intuitionistic Implication},
	booktitle={Logic in Computer Science},
	year={1991},
	month={July}
}

@inproceedings{
	lipton,
	author={J. Lipton},
	title={Kripke Semantics for Dependent Type Theory and
		Realizabity Interpretations},
	booktitle={these proceedings},
	year={1991}
}

@book{
	no-enumeration-total-comp,
	author={M. Machtey and P. Young},
	title={An Introduction to the General Theory of Algorithms},
	publisher={North-Holland},
	year={1978}
}

@incollection{
	MitchTCS,
	Author="J. C. Mitchell",
        Title="Type systems for programming languages",
        Booktitle="Handbook of Theoretical Computer
        Science, Volume B",
        editor="J. van Leeuwen",
        publisher="North-Holland",
        Address="Amsterdam",
        Year="1990",
        pages="365--458"
}

@article{
	peirce:algebra-of-logic,
	author = {C. S. Peirce},
	title  = {On the Algebra of Logic: A Contribution to the
		  Philosophy of Notation},
	journal= {American Journal of Mathematics},
	volume = {8},
	year   = {1885},
	pages  = {180--202}
}

@inproceedings{
        pitts,
        author={Andrew M.\ Pitts},
        title={Poloymorphism is Set-Theoretic, Constructively},
        booktitle={Proceedings of the Conference on Category Theory
		  and Computer Science, Edinburgh, 1987},
        editor={D.\ Pitt},
        series={Lecture Notes in Computer Science},
        volume={283},
        publisher={Springer-Verlag},
        address={Berlin},
        year={1987},
        pages={12--39}
}

@inproceedings{
	pratt,
	author={V. R. Pratt},
	title={Semantical Considerations on {Floyd}-{Hoare} Logic},
	booktitle={17th  Annual Symposium on Foundations of Computer Science},
	year={1976},
	pages={109--121},
	organization={IEEE},
	month={October}}

@book{
	prawitz,
	author={D. Prawitz},
	title={Natural Deduction},
	publisher={Almqvist \& Wiksell},
	address={Stockholm},
	year={1965}
}

@inbook{
        reynolds,
        author={John C.\ Reynolds},
        title={Polymorphism is Not Set-Theoretic},
        booktitle={Semantics of Data Types},
        series={Lecture Notes in Computer Science},
        volume={173},
        publisher={Springer-Verlag},
        address={Berlin},
        year={1984},
        pages={145--156}
}

@article{
	rose,
	author={G. F. Rose},
	title={Propositional Calculus and Realizability},
	journal={Transactions of the American Mathematical Society},
	year={1953},
	volume={75},
	month={July--September},
	pages={1--19}
}

@article{
	nonstandard-arithmetic,
	author={T. Skolem},
	title={\"{U}ber die {Nicht}-charak\-ter\-isier\-bar\-keit
		der {Zahlenreihe} mittels
		endlich oder abz\"ahlbar unendlich vieler {Aussagen} mit
		ausschlie{\ss}lich {Zahlenvariablen}},
	journal={Fundamenta Mathematicae},
	year={1934},
	volume={23},
	pages={150--161},
	note={Reprinted in~\cite{fenstad}}
}

@book{
	fenstad,
	editor={J. E. Fenstad},
	title={Selected Works in Logic},
	publisher={Universitetsforlaget},
	year={1970}
}

@article{
	constructive-satisfiability,
	author={R. Statman},
	title={Intuitionistic Propositional Logic is
		Polynomial-Space Complete},
	journal={Theoretical Computer Science},
	volume={9},
	number={1},
	year={1979},
	pages={67--72}
}

@article{
	StatRel,
	author="R. Statman",
        Title="Logical Relations and the Typed Lambda Calculus",
        Journal="Information and Control",
        Volume="65", year="1985",
        pages="85--97"}

@book{
	stenlund,
	author={S\"oren Stenlund},
	title ={Combinators, $\lambda$-terms, and Proof Theory},
	publisher={D. Riedel Publishing Company},
	address={Dordrecht-Holland},
	year={1972}
}

@article{
	tarski:classical-semantics,
	author={Alfred Tarski},
	title={Poj{\c e}cie Prawdy W J{\c e}zykach Nauk Dedukcyjnch},
	journal={Prace Towarzystwa Naukowego Warzawskiego},
	note={English translation in \cite{tarski:works}},
	year={1933}
}

@book{
	tarski:works,
	author={Alfred Tarski},
	title={Logic, Semantics, and Metamathematics},
	publisher={Oxford University Press},
	year={1956}
}

@book{
	Troelstra,
	author="A. S. Troelstra",
	title="Mathematical Investigation of Intuitionistic Arithmetic and
		Analysis",
	publisher="Springer-Verlag",
	Address="Berlin",
	series="Lecture Notes in Mathematics", volume="344",
	year="1973"}

@book{
	troelstra:choice-seq,
	author={A.S. Troelstra},
	title={Choice Sequences: a chapter of intuitionistic mathematics},
	publisher={Clarendon Press},
	address={Oxford},
	year={1977},
	series={Oxford Logic Guides}
}

@book{
	troelstra-van-dalen,
	author={A. S. Troelstra and D. van Dalen},
	title={Constructivism in Mathematics: an Introduction},
	publisher={North-Holland},
	year={1988},
	series={Studies in Logic and the Foundations of Mathematics},
}

@article{
	turing:entscheidungsproblem,
	author = {A. M. Turing},
	title = {On Computable Numbers, With an Application to the
		 {Entscheidungsproblem}},
	journal = {Proceedings of the London Mathematical Society,
		   Second Series},
	year = {1937},
	volume = {42},
	pages = {230--265}
}

@incollection{
	van-benthem,
	author={Johan van Benthem},
	title={Correspondence Theory},
	booktitle={Handbook of Philosophical Logic, Volume 2:
		   Extensions of Classical Logic},
	publisher={D. Reidel},
        address={Dordrecht},
	year={1984},
	pages={167--247}
}

@incollection{
        van-dalen,
        author={D.\ {van Dalen}},
        title={Intuitionistic Logic},
        booktitle={Handbook of Philosophical Logic III},
        editor={D.\ Gabbay and F.\ Guenther},
        publisher={D.\ Reidel},
        address={Dordrecht},
        year={1986},
        pages={225--339}
}

@article{
        veldman,
        author={W.\ Veldman},
        title={An Intuitionistic Completeness Theorem for
		  Intuitionistic Predicate Logic},
        journal={Journal of Symbolic Logic},
        volume={41},
        year={1976},
        pages={159--166}
}

@article{
	wittgenstein:tractatus,
	author={L. Wittgenstein},
	title={Tractatus Logico-Philo\-sophicus},
	year={1921},
	journal={Annalen der {Natur}-philo\-sophie},
	note={English translation in~\cite{wittgenstein:tractatus-english}}
}

@book{
	wittgenstein:tractatus-english,
	author={L. Wittgenstein},
	title={Tractatus Logico-Philo\-sophicus},
	year={1961},
	publisher={Routledge and Kegan Paul}
}