Realizability Bibliography

Additions and corrections are very welcome. Please email them to Lars Birkedal (birkedal@itu.dk).

Search the Bibliography

  Keywords: 
  Authors:  
              
  

• M. Abadi and G.D. Plotkin. A per model of polymorphism and recursive types. In J. Mitchell, editor, 5th Annual IEEE Symposium on Logic in Computer Science, pages 355-365, Philadelphia, 1990. IEEE Computer Society Press.

• M. Abadi and L. Cardelli. A Theory of Objects. Springer Verlag, 1996.

• S. Abramsky. Typed realizability. Talk at the workshop on Category Theory and Computer Science in Cambridge, England, August 1995.

• P.H.G. Aczel. A note on interpreting intuitionistic higher-order logic, 1980. Handwritten note.

• T. Altenkirch. Constructions, Inductive Types and Strong Normalization. PhD thesis, University of Edinburgh, 1993. Available as report ECS-LFCS-93-279.

• R. Amadio. Recursion over realizability structures. Information and Computation, 91:55-85, 1991.

• A. Asperti. The internal model of polymorphic lambda calculus. Technical Report CMU-CS-88-155, Carnegie Mellon University, 1988.

• J. Avigad. A realizability interpretation for classical arithmetic. In Buss, Hájek, and Pudlák, editors, Logic Colloquium '98, number 13 in Lecture Notes in Logic, pages 57-90. AK Peters, 2000.

• S. Awodey, L. Birkedal, and D.S. Scott. Local realizability toposes and a modal logic for computability. Presented at Tutorial Workshop on Realizability Semantics, FLoC'99, Trento, Italy 1999., 1999.

• S. Bainbridge, P.J. Freyd, A. Scedrov, and P. Scott. Functorial polymorphism. Theoretical Computer Science, 70:35-64, 1990.

• F. Barbanera and S. Martini. Proof-functional connectives and realizability. Archive for Mathematical Logic, 33:189-211, 1994.

• H.P. Barendregt. Combinatory logic and the axiom of choice. Indagationes Mathematicae, 35:203-221, 1973.

• H.P. Barendregt. Introduction to generalized type systems. Journal of Functional Programming, 1(2):125-154, 1991.

• M. Barr. Exact categories. In M. Barr, P.A. Grillet, and D. Van Osdol, editors, Exact Categories and Categories of Sheaves, volume 236 of Lecture Notes in Mathematics, pages 1-120. Springer-Verlag, 1971.

• A. Bauer, L. Birkedal, and D.S. Scott. Equilogical spaces. Submitted for publication, 1998.

• M.J. Beeson and A. Scedrov. Church's thesis, continuity and set theory. Journal of Symbolic Logic, 49:630-643, 1984.

• M.J. Beeson. Continuity and comprehension in intuitionistic formal systems. Pacific Journal of Mathematics, 68:29-40, 1977.

• M.J. Beeson. Continuity in intuitionistic set theories. In M. Boffa, D. van Dalen, and K. McAloon, editors, Logic Colloquium '78, pages 1-52. North-Holland Publishing Company, 1979.

• M.J. Beeson. Derived rules of inference related to the continuity of effective operations. Journal of Symbolic Logic, 41:328-336, 1976.

• M.J. Beeson. Extensionality and choice in constructive mathematics. Pacific Journal of Mathematics, 88:1-28, 1980.

• M.J. Beeson. Formalizing constructive mathematics: Why and how?. In F. Richman, editor, Constructive Mathematics, pages 146-190. Springer-Verlag, 1981.

• M.J. Beeson. Foundations of constructive mathematics. Springer-Verlag, 1985.

• M.J. Beeson. The nonderivability in intuitionistic formal systems of theorems on the continuity of effective operations. Journal of Symbolic Logic, 41:321-346, 1975.

• M.J. Beeson. Principles of continuous choice and continuity of functions in formal systems for constructive mathematics. Arhive for Mathematical Logic, 12:249-322, 1977.

• M.J. Beeson. Recursive models for constructive set theories. Annals of Pure and Applied Logic, 23:127-178, 1982.

• M.J. Beeson. The unprovability in intuitionistic formal systems of continuity of effective operations on the reals. Journal of Symbolic Logic, 41:18-24, 1976.

• M.J. Beeson. Goodman's theorem and beyond. Pacific Journal of Mathematics, 84:1-28, 1979.

• Z.E-L. Benaissa, E. Moggi, W. Taha, and T. Sheard. A categorical analysis of multi-level languages. Manuscript, January 1999.

• P.N. Benton. A mixed linear and non-linear logic: Proofs, terms and models (preliminary report). Technical report, University of Cambridge, 1995.

• S. Berardi, M.A. Bezem, and T. Coquand. On the computational content of the axiom of choice. Technical Report Logic Group Preprint Series, 116, Department of Philosophy, Utrecht University, 1994.

• U. Berger and H. Schwichtenberg. Program extraction from classical proofs. In D. Leivant, editor, Logic and Computational Complexity. International Workshop LCC '94, Indianapolis, IN, USA, October 1994, volume 960 of Lecture Notes in Computer Science, pages 77-97. Springer-Verlag, 1995.

• U. Berger, H. Schwichtenberg, and M. Seisenberger. From proofs to programs in the Minlog system. The Warshall algorithm and Higman's lemma, 1997. To appear in Journal of Automated Reasoning.

• I. Bethke. Notes on Partial Combinatory Algebras. PhD thesis, Universiteit van Amsterdam, 1988.

• M. Bezem. Bar Recursion and Functionals of Finite Type. PhD thesis, Rijksuniversiteit Utrecht, 1986.

• M. Bezem. Compact and majorizable functionals of finite type. Journal of Symbolic Logic, 54:271-280, 1989.

• M. Bezem. Strongly majorizable functionals of finite type: a model for bar recursion containing discontinuous functionals. Journal of Symbolic Logic, 50:652-660, 1985.

• L. Birkedal. Developing Theories of Types and Computability. PhD thesis, School of Computer Science, Carnegie Mellon University, December 1999.

• L. Birkedal, A. Carboni, G. Rosolini, and D.S. Scott. Type theory via exact categories. In Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, pages 188-198, Indianapolis, Indiana, June 1998. IEEE Computer Society Press.

• K. Bruce and J.C. Mitchell. Per models of subtyping, recursive types and higher-order polymorphism. In Proc. 19th ACM Symp. on Principles of Programming, pages 316-327, 1992.

• W. Buchholz, S. Feferman, W. Pohlers, and W. Sieg. Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies. Springer-Verlag, 1981.

• S. Buss. The polynomial hierarchy and intuitionistic bounded arithmetic. In Structure in Complexity Theory, volume 223 of Springer Lecture Notes in Computer Science, pages 77-103. Springer-Verlag, 1986.

• A. Carboni, P.J. Freyd, and A. Scedrov. A categorical approach to realizability and polymorphic types. In M. Main, A. Melton, M. Mislove, and D.Schmidt, editors, Mathematical Foundations of Programming Language Semantics, volume 298 of Lectures Notes in Computer Science, pages 23-42, New Orleans, 1988. Springer-Verlag.

• A. Carboni and R. Celia Magno. The free exact category on a left exact one. Journal of Australian Mathematical Society, 33(A):295-301, 1982.

• A. Carboni and G. Rosolini. Locally cartesian closed exact completions, 1998. to appear.

• A. Carboni and E.M. Vitale. Regular and exact completions. Journal of Pure and Applied Algebra, 125:79-117, 1998.

• A. Carboni. Some free constructions in realizability and proof theory. Journal of Pure and Applied Algebra, 103:117-148, 1995.

• L. Cardelli and G. Longo. A semantic basis for Quest. Technical Report 55, Digital Equipment Corporation, 1989.

• C. Cellucci. Operazioni di Brouwer e realizzabilita formalizzata (English summary). Annali della Scuola Normale Superiore di Pisa. Classe di Science. Fisiche e Matiche, Seria III, 25:649-682, 1971.

• S. Cook and A. Urquhart. Functional interpretations of feasibly constructive arithmetic. Annals of Pure and Applied Logic, 63:103-200, 1993.

• Th. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76, 1988.

• T. Coquand, C. Gunter, and G. Winskel. Domain theoretic models of polymorphism. Information and Computation, 81:123-167, 1989.

• Th. Coquand. Une Theorie des Constructions. PhD thesis, University of Paris VII, 1985.

• N.J. Cutland. Computability. Cambridge University Press, 1980.

• Z. Damnjanovic. Elementary realizability, 1996. Submitted to Journal of Philosophical Logic.

• Z. Damnjanovic. Minimal realizability of intuitionistic arithmetic and elementary analysis. Journal of Symbolic Logic, 60:1208-1241, 1995.

• Z. Damnjanovic. Strictly primitive recursive realizability, I. Journal of Symbolic Logic, 59:1210-1227, 1994.

• D.H.J. de Jongh. A characterization of the intuitionistic propositional calculus. In A. Kino, J. R. Myhill, and R. E. Vesley, editors, Intuitionism and Proof Theory, pages 211-217. North-Holland Publishing Company, 1970.

• D.H.J. de Jongh. Formulas of one propositional variable in intuitionistic arithmetic. In A. S. Troelstra and D. van Dalen, editors, The L. E. J. Brouwer Centenary Symposium, pages 51-64. North-Holland Publishing Company, 1980.

• D.H.J. de Jongh. Investigations of the Intuitionistic Propositional Calculus. PhD thesis, University of Wisconsin, Madison, 1968.

• D.H.J. de Jongh. The maximality of the intuitionistic predicate calculus with respect to heyting's arithmetic, 1969. typed manuscript from University of Winsconsin, Madison.

• J. Diller and W. Nahm. Eine Variante zur Dialectica--Interpretation der Heyting--Arithmetik endlicher Typen. Archiv, 16:49-66, 1974.

• J. Diller. Functional interpretations of Heyting's arithmetic in all finite types. Nieuw Archief voor Wiskunde. Derde Serie, 27:70-97, 1979.

• J. Diller. Modified realization and the formulae-as-types notion. In J. P. Seldin and J. R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 491-501. Academic Press, New York, 1980.

• A.G. Dragalin. An algebraic approach to intuitionistic models of the realizability type (Russian). In A. I. et.al. Mikhajlov, editor, Issledovaniya po Neklassicheskim Logikam i Teorii Mnozhestv (Investigations on Non-Classical Logics and Set Theory), pages 83-201. Nauka, Moskva, 1979.

• A.G. Dragalin. The computability of primitive recursive terms of finite type, and primitive recursive realization (Russian). Zapiski, 8:32-45, 1968. Translation Seminars in Mathematics. V.A.Steklov Mathematical Institute Leningrad 8(1970), pp. 13-18. This volume appeared as: A.O. Slisenko (ed.), Studies in Constructive Mathematics and Mathematical Logic. Part II. Consultants Bureau, New York, London.

• A.G. Dragalin. Mathematical Intuitionism. American Mathematical Society, 1988. Translation of the Russian original from 1979.

• A.G. Dragalin. New forms of realizability and Markov's rule (Russian). Doklady, 251:534-537, 1980. Translation SM 21, pp. 461-464.

• A.G. Dragalin. Transfinite completions of constructive arithmetical calculus (Russian). Doklady, 189:458-460, 1969. Translation SM 10, pp. 1417-1420.

• P. Eggerz. Realisierbarkeitskalküle ML₀ und vergleichbare Theorien im Verhältnis zur Heyting-Arithmetik. PhD thesis, Ludwig-Maximilians-Universität, München, 1987.

• Th. Ehrhard. A categorical semantics of constructions. In Proc. of 3rd Annual Symposium on Logic in Computer Science. IEEE Computer Soc. Press, 1988.

• Yu.L. Er v sov. Computable functionals of finite type. Algebra i Logika, 11(4), 1972.

• Yu.L. Er v sov. Model sf C of partial continuous functionals. In R.O. Gandy and J.M.E. Hyland, editors, Logic Colloquium '77, pages 455-467. North Holland Publishing Company, 1977.

• Yu.L. Er v sov. The theory of A-spaces. Algebra i Logika, 12(4), 1972.

• Yu.L. Er v sov. Theorie der Numerierungen. Zeitschrift für Math. Log., 19(4):289-388, 1973.

• Yu.L. Er v sov. Theorie der Numerierungen II. Zeitschrift für Math. Log., 21(6):473-584, 1975.

• Yu.L. Er v sov. Theorie der Numerierungen III. Zeitschrift für Math. Log., 23(4):289-371, 1977.

• S. Feferman. Constructive theories of functions and classes. In M. Boffa, D. van Dalen, and K. McAloon, editors, Logic Colloquium '78, pages 159-224. North-Holland Publishing Company, 1979.

• S. Feferman. A language and axioms for explicit mathematics. In J.N. Crossley, editor, Algebra and Logic, pages 87-139. Springer-Verlag, 1975.

• F. Ferreira and A. Marques. Extracting algorithms from intuitionistic proofs. Technical Report Pré-publicações de Matemática 26/96, Universidade de Lisboa, 1996.

• M.P. Fourman and D.S. Scott. Sheaves and logic. In M.P. Fourman, C.J. Mulvey, and D.S. Scott, editors, Applications of Sheaves, pages 302-401. Springer-Verlag, 1979.

• P.J. Freyd and A. Scedrov. Categories, Allegories. North Holland Publishing Company, 1991.

• P.J. Freyd, E.P. Robinson, and G. Rosolini. Dinaturality for free. In M.P. Fourman, P.T. Johnstone, and A.M. Pitts, editors, Proceedings of Symposium in Applications of Categories to Computer Science, pages 107-118. Cambridge University Press, 1992.

• P.J. Freyd, P. Mulry, G. Rosolini, and D.S. Scott. Extensional PERs. Information and Computation, 98:211-227, 1992.

• P.J. Freyd. POLYNAT in PER. In J.W. Gray and A. Scedrov, editors, Categories in Computer Science and Logic, volume 92 of Contemporary Mathematics, pages 67-68, Boulder, June 1987, 1989. American Mathematical Society.

• H.M. Friedman. Some applications of Kleene's methods for intuitionistic systems. In A. R. D. Mathias and H. Rogers, editors, Cambridge Summer School in Mathematical Logic, pages 113-170. Springer-Verlag, 1973.

• H.M. Friedman. On the derivability of instantiation properties. Journal of Symbolic Logic, 42:506-514, 1977.

• H.M. Friedman. The disjunction property implies the numerical existence property. Proceedings of the National Academy of Sciences of the United States of America, 72:2877-2878, 1975.

• H.M. Friedman and A. Scedrov. Intuitionistically provable recursive well-orderings. Annals of Pure and Applied Logic, 30:165-171, 1986.

• H.M. Friedman and A. Scedrov. Large sets in intuitionistic set theory. Annals of Pure and Applied Logic, 27:1-24, 1984.

• H. M. Friedman and A. Scedrov. Set existence property for intuitionistic theories with dependent choice. Annals of Pure and Applied Logic, 25:129-140, 1983. Corrigendum in APAL 26 (1984), p.101.

• H.M. Friedman. Set theoretic foundations of constructive analysis. Annals of Mathematics, Series 2, 105:1-28, 1977.

• J. Gallier. Proving properties of typed lambda-terms using realizability, covers, and sheaves. Technical Report MS-CIS-93-91, Computer and Information Science Department, School of Engineering and Applied Science, University of Pennsylvania, Philadelphia, 1993.

• R.O. Gandy and J.M.E. Hyland. Computable and recursively countable functions of higher type. In Logic Colloquium '76. North-Holland, 1977.

• Yu. V. Gavrilenko. Recursive realizability from the intuitionistic point of view (Russian). Doklady, 256:18-22, 1981. Translation SM 23, pp. 9-14.

• J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

• J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, Cambridge U.K., 1988.

• K. Gödel. Collected Works, Volume 2. Oxford University Press, Oxford, 1990.

• K. Gödel. Zur intuitionistischen arithmetik und zahlentheorie. Ergebnisse eines mathematisches Kolloquiums, 4:34-38, 1932.

• K. Gödel. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica, 12:280-287, 1958.

• N.D. Goodman. Relativized realizability in intuitionistic arithmetic of all finite types. Journal of Symbolic Logic, 43:23-44, 1978.

• R.J. Grayson. Heyting-valued models for intuitionistic set theory. In M. Fourman, C. Mulvey, and D.S. Scott, editors, Application of Sheaves, volume 743 of Lecture Notes in Mathematics, pages 402-414, Berlin, 1979. Springer.

• R.J. Grayson. Appendix to modified realisability toposes, 1982. Handwritten notes from Münster University.

• R.J. Grayson. Derived rules obtained by a model-theoretic approach to realisability, 1981. Handwritten notes from Münster University.

• R.J. Grayson. Note on extensional realizability, 1981. Handwritten notes from Münster University.

• R.J. Grayson. Modified realisability toposes, 1981. Handwritten notes from Münster University.

• R. Grayson. Notes on realizability, 1982.

• V. Harnik and M. Makkai. Lambek's categorical proof theory and Läuchli's abstract realizability. Journal of Symbolic Logic, 57:200-230, 1992.

• V. Harnik. Provably total functions of intuitionistic bounded arithmetic. Journal of Symbolic Logic, 57:466-477, 1992.

• A. Heyting, editor. Constructivity in Mathematics. North-Holland Publishing Company, 1959.

• D. Higgs. Injectivity in the topos of complete heyting algebra valued sets. Canadian Journal of Mathematics, 36(3):550-568, 1984.

• D. Hilbert and P. Bernays. Grundlagen der Mathematik I. Springer Verlag, 1934.

• M. Hofmann. Semantical analysis of higher-order abstract syntax. In 14th Annual Symposium on Logic in Computer Science, pages ?--? IEEE Computer Society Press, Washington, 1999.

• M. Hofmann. Syntax and semantics of dependent types. In Semantic and Logic of Computation. Cambridge University Press, 1997.

• W.A. Howard. Appendix: Hereditarily majorizable functionals of finite type. In A. S. Troelstra, editor, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, pages 454-461. Springer-Verlag, 1973. With contributions by A. S. Troelstra, A. Smorynski, J. I. Zucker and W. A. Howard.

• W.A. Howard. To H.B. Curry: The formulae-as-types notion of construction. In J. Hindley and J. Seldin, editors, Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, 1969.

• J.M.E. Hyland, E.P. Robinson, and G. Rosolini. Algebraic types in PER models. In M. Main, A. Melton, M. Mislove, and D.Schmidt, editors, Mathematical Foundations of Programming Language Semantics, volume 442 of Lecture Notes in Computer Science, pages 333-350, New Orleans, 1990. Springer-Verlag.

• J.M.E. Hyland, E.P. Robinson, and G. Rosolini. The discrete objects in the effective topos. Proceedings of the London Mathematical Society, 60:1-60, 1990.

• J.M.E. Hyland. The effective topos. In A.S. Troelstra and D. Van Dalen, editors, The L.E.J. Brouwer Centenary Symposium, pages 165-216. North Holland Publishing Company, 1982.

• J.M.E. Hyland. First steps in synthetic domain theory. In A. Carboni, M.C. Pedicchio, and G. Rosolini, editors, Category Theory '90, volume 1144 of Lectures Notes in Mathematics, pages 131-156, Como, 1992. Springer-Verlag.

• J.M.E. Hyland. Filter spaces and continuous functionals. Annals of Mathematical Logic, 16, 1979.

• J.M.E. Hyland and C.-H. L. Ong. Modified realizability toposes and strong normalization proofs. In J.F. Groote and M. Bezem, editors, Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, pages 179-194. Springer-Verlag, 1993.

• J.M.E. Hyland. A small complete category. Journal of Pure and Applied Logic, 40:135-165, 1988.

• J.M.E. Hyland, P.T. Johnstone, and A.M. Pitts. Tripos theory. Math. Proc. Camb. Phil. Soc., 88:205-232, 1980.

• B. Jacobs. Categorical Logic and Type Theory. Elsevier Science, 1999.

• V.A. Jankov. Realizable formulas of propositional logic (Russian). Doklady, 151:1035-1037, 1963. Translation SM 4, pp. 1146-1148.

• P.T. Johnstone and R. Paré, editors. Indexed Categories and Their Applications, volume 661 of Lecture Notes in Mathematics. Sringer-Verlag, Berlin, 1978.

• P.T. Johnstone and E.P. Robinson. A note on inequivalence of realizability toposes. Mathematical Proceedings of Cambridge Philosophical Society, 105, 1989.

• P.T. Johnstone and I. Moerdijk. Local maps of toposes. Proc. London Math. Soc., 3(58):281-305, 1989.

• P.T. Johnstone. Topos Theory. Number 10 in LMS Mathematical Monographs. Academic Press, London, 1977.

• A. Joyal and I. Moerdijk. Algebraic Set Theory, volume 220 of London Mathematical Society Lecture Note Series. Cambridge University Press, Cambridge, 1995.

• F.A. Kabakov. On the derivability of some realizable formulae of the sentential calculus (Russian). ZMLG, 9:97-104, 1963.

• F.A. Kabakov. Intuitionistic deducibility of some realizable formulae of propositional logic (Russian). Doklady, 192:269-271, 1970. Translation SM 11, pp. 612-614.

• F.A. Kabakov. On modelling of pseudo-boolean algebras by realizability (Russian). Doklady, 192:16-18, 1970. Translation SM 11, pp. 562-564.

• G.M. Kelly and F.W. Lawvere. On the complete lattice of essential localizations. Bull. Soc. Math. Belg. Ser. A, XLI(2):289-319, 1989.

• V. Kh. Khakhanyan. Comparative strength of variants of Church's thesis at the level of set theory (Russian). Doklady, 252:1070-1074, 1980. Translation SM 21, pp. 894-898.

• V. Kh. Khakhanyan. The consistency of some intuitionistic and constructive principles with a set theory. Studia Logica, 40:237-248, 1981.

• V. Kh. Khakhanyan. Consistency of the intuitionistic set theory with Brouwer's principle. Matematika, 5, 1979.

• V. Kh. Khakhanyan. The consistency of intuitionistic set theory with Church's principle and the uniformization principle (Russian). Vestnik Moskovskogo Universiteta. Seriya I. Matematika, Mekhanika, 5:3-7, 1980. Translation Moscow University Mathematics Bulletin 35/5, pp. 3-7.

• V. Kh. Khakhanyan. The consistency of intuitionistic set theory with formal mathematical analysis (Russian). Doklady, 253:48-52, 1980. Translation SM 22, pp. 46-50.

• V. Kh. Khakhanyan. Nonderivability of the uniformization principle from Church's thesis (Russian). Matematicheskie Zametki, 43:685-691,703, 1988. Translation Mathematical Notes 43, pp. 394-398.

• V. Kh. Khakhanyan. Set theory and Church's thesis (Russian). In A. I. Mikhajlov, editor, Issledovaniya po Neklascheskims Logikam i Formal'nym Sistemam (Studies in Nonclassical logics and Formal Systems), pages 198-208. Nauka, Moskva, 1983.

• M.M. Kipnis. The constructive classification of arithmetic predicates and the semantic bases of arithmetic (Russian). Zapiski, 8:53-65, 1968. Translation Seminars in Mathematics. V.A.Steklov Mathematical Institute Leningrad 8(1970), pp. 22-27. This volume appeared as: A.O. Slisenko (ed.), Studies in Constructive Mathematics and Mathematical Logic. Part II. Consultants Bureau, New York, London.

• M.M. Kipnis. On the realizations of predicate formulas (Russian) (English summary). Zapiski, 20:40-48, 1971. Translation Journal of Soviet Mathematics 1(1973), pp. 22-27.

• S.C. Kleene. Classical extensions of intuitionistic mathematics. In Y. Bar-Hillel, editor, LMPS 2, pages 31-44. North-Holland Publishing Company, 1965.

• S.C. Kleene. Constructive functions in ``The Foundations of Intuitionistic Mathematics''. In B. van Rootselaar and J. F. Staal, editors, LMPS 3, pages 137-144. North-Holland Publishing Company, 1968.

• S.C. Kleene. Countable functionals. In A. Heyting, editor, Constructivity in Mathematics, pages 81-100. North Holland Publishing Company, 1959.

• S.C. Kleene. Disjunction and existence under implication in elementary intuitionistic formalisms. Journal of Symbolic Logic, 27:11-18, 1962. Addenda in JSL 28 (1963), pp. 154-156.

• S.C. Kleene. Recursive functionals and quantifiers of finite types II. Trans. Amer. Math. Soc, 108, 1963.

• S.C. Kleene. Formalized Recursive Functionals and Formalized Relizability, volume 89 of Memoirs of the American Mathematical Society. American Mathematical Society, 1969.

• S.C. Kleene and R.E. Vesley. The Foundations of Intuitionistic Mathematics, especially in relation to recursive functions. North-Holland Publishing Company, 1965.

• S.C. Kleene. On the interpretation of intuitionistic number theory. Journal of Symbolic Logic, 10:109-124, 1945.

• S.C. Kleene. Introduction to metamathematics. North-Holland Publishing Company, 1952. Co-publisher: Wolters-Noordhoff; 8th revised ed.1980.

• S.C. Kleene. Logical calculus and realizability. Acta Philosophica Fennica, 18:71-80, 1965.

• S. C. Kleene. Realizability. In Summaries of Talks presented at the Summer Institute for Symbolic Logic, pages 100-104. Institute for Defense Analyses, Communications Research Division, Princeton, 1957. Also in [109], pp. 285-289. Errata in [150], page 192.

• S.C. Kleene. Realizability: a retrospective survey. In A.R.D. Mathias and H. Rogers, editors, Cambridge Summer School in Mathematical Logic, volume 337 of Lecture Notes in Mathematics, pages 95-112. Springer-Verlag, 1973.

• S.C. Kleene. Realizability and Shanin's algorithm for the constructive deciphering of mathematical sentences. Logique et Analyse, Nouvelle Série, 3:154-165, 1960.

• S.C. Kleene. Recursive functionals and quantifiers of finite types I. Trans. Amer. Math. Soc, 91, 1959.

• S.C. Kleene. Recursive functionals and quantifiers of finite types revisited I. In J.E. Fenstad, R.O. Gandy, and G.E. Sacks, editors, Generalized Recursion Theory II, pages 185-222, 1978.

• S. Kobayashi and M. Tatsuta. Realizability interpretation of generalized inductive definitions. Theoretical Computer Science, 131:121-138, 1994.

• U.W. Kohlenbach. Pointwise hereditary majorization and some applications. Archive for Mathematical Logic, 31:227-241, 1992.

• U.W. Kohlenbach. Theorie der majorisierbaren und stetigen Funktionale und ihre Anwendung bei der Extraktion von Schranken aus inkonstruktiven Beweisen: effektive Eindeutigkeitsmodule bei besten Approximationen aus ineffektiven Eindeutigkeitsbeweisen. PhD thesis, J.W. Goethe-Universität, Frankfurt am Main, 1990.

• G. Kreisel and A.S. Troelstra. Formal systems for some branches of intuitionistic analysis. Annals of Pure and Applied Logic, 1:229-387, 1970. Addendum in APAL 3, pp. 437-439.

• G. Kreisel. Foundations of intuitionistic logic. In E. Nagel, P. Suppes, and A. Tarski, editors, LMPS, pages 198-210. Stanford University Press, Stanford, 1962.

• G. Kreisel. Interpretation of analysis by means of functionals of finite type. In A. Heyting, editor, Constructivity in Mathematics, pages 101-128. North-Holland, 1959.

• G. Kreisel. A variant to Hilbert's theory of the foundations of arithmetic. British Journal for the Philosophy of Science, 4:107-127, 1953.

• G. Kreisel. On weak completeness of intuitionistic predicate logic. Journal of Symbolic Logic, 27:139-158, 1962.

• M.D. Krol'. Disjunctive and existential properties of intuitionistic analysis with Kripke's scheme (Russian). Doklady, 234, 1977. Translation SM 18, pp. 755-758.

• M.D. Krol'. Various forms of the continuity principle (Russian). Doklady, 271:33-36, 1983. Translation SM 28, pp. 27-30.

• M.D. Krol'. On a version of realizability (Russian). In XI Interrepublican Conference on Mathematical Logic, University of Kazan, October 6-8, 1992, page 81, 1992.

• S.A. Kurtz, J.C. Mitchell, and M.J. O'Donnell. Connecting formal semantics to constructive intuitions. Technical Report CS 92-01, Department of Computer Science, University of Chicago, 1992.

• J. Lambek and P.J. Scott. Independence of premisses and the free topos. In Proc. Symp. Constructive Math, volume 873 of Lecture Notes in Mathematics, pages 191-207, 1981.

• J. Lambek and P. J. Scott. Introduction to Higher Order Categorical Logic. Cambridge University Press, Cambridge, 1986.

• J. Lambek and P.J. Scott. Intuitionistic type theory and the free topos. Journal of Pure and Applied Algebra, 19:215-257, 1980.

• J. Lambek and P.J. Scott. New proofs of some intutitionistic principles. Zeitschrift für Math. Log., 29:493-504, 1983.

• H. Läuchli. An abstract notion of realizability for which intuitionistic predicate calculus is complete. In A. Kino, J.R. Myhill, and R.E. Vesley, editors, Intuitionism and Proof Theory, pages 227-234. North-Holland, 1970.

• F.W. Lawvere. Adjointness in foundations. Dialectica, 23:281-296, 1969.

• F. W. Lawvere. Diagonal arguments and cartesian closed categories. In Category Theory, Homology Theory and their Applications, II (Battelle Institute Conference, Seattle, Wash., 1968, Vol. Two), pages 134-145. Springer-Verlag, Berlin, 1969.

• F.W. Lawvere. Equality in hyperdoctrines and the comprehension schema as an adjoint functor. In A. Heller, editor, Applications of Categorical Algebra, pages 1-14. American Mathematical Society, Providence RI, 1970.

• F.W. Lawvere. Some thoughts on the future of category theory. In A. Carboni, M.C. Pedicchio, and G. Rosolini, editors, Category Theory. Proceedings of the International Conference held in Como, Italy, July 22-28, 1990, volume 1488 of Lecture Notes in Mathematics, pages 1-13. Springer-Verlag, 1991.

• F.W. Lawvere. Toposes generated by codiscrete objects in combinatorial topology and functional analysis. Notes for Colloquium lectures given at North Ryde, New South Wales, Australia on April 18, 1989 and at Madison, USA, on December 1, 1989, 1989.

• D. Leivant. Contracting proofs to programs. In P. Odifreddi, editor, Logic and Computer Science, pages 279-327. Academic Press, London, 1990.

• D. Leivant. Peano's lambda calculus: The functional abstraction implicit in arithmetic. In C.A. Anderson and M. Zeleny, editors, Church Memorial Volume: Logic, Language, and Computation. Kluwer Academic Publishing, 2000. To Appear.

• D. Leivant. Peano's lambda calculus: The functional abstraction implicit in arithmetic. Bulletin of Symbolic Logic, 4:451-452, 1998.

• D. Leivant. Ramified recurrence and computational complexity III: Higher type recurrence and elementary complexity. Annals of Pure and Applied Logic, 96(3):209-229, 1999.

• D. Leivant. Reasoning about functional programs and complexity classes associated with type disciplines. In Proceedings of the Twenty Fourth Annual Symposium on the Foundations of Computer Science, pages 460-469. IEEE Computer Society, Washington, 1983.

• V. Lifschitz. Calculable natural numbers. In S. Shapiro, editor, Intensional Mathematics, pages 173-190. North-Holland, 1985.

• V. Lifschitz. Constructive assertions in an extension of classical mathematics. Journal of Symbolic Logic, 47:359-387, 1982.

• V. Lifschitz. CT₀ is stronger than CT₀!. Proceedings of the American Mathematical Society, 73:101-106, 1979.

• J. Lipton. Constructive Kripke semantics and realizability. In Y.N. Moschovakis, editor, Logic from Computer Science. Springer, 1990. Also as a Technical Report, from Cornell University, nr.90-71.

• J. Lipton and M.J. O'Donnell. Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels. Annals of Pure and Applied Logic, 81:187-239, 1996.

• J. Longley. Realizability Toposes and Language Semantics. PhD thesis, Edinburgh University, 1995.

• J. Longley. The sequentially realizable functionals. Technical Report ECS-LFCS-98-402, University of Edinburgh, 1998.

• J.R. Longley and A.K. Simpson. A uniform approach to domain theory in realizability models. Mathematical Structures in Computer Science, 7:469-505, 1997.

• G. Longo and E. Moggi. Cartesian closed categories of enumerations for effective type structures. In G. Kahn, D. MacQueen, and G. Plopkin, editors, Semantics of Data Types, volume 173 of Lecture Notes in Computer Science. Springer-Verlag, 1984.

• G. Longo and E. Moggi. Constructive natural deduction and its omega -set interpretation. Mathematical Structures in Computer Science, 1:215-254, 1991.

• G. Longo and E. Moggi. The hereditary partial effective functionals and recurion theory in higher type. Journal of Symbolic Logic, 49:127-140, 1984.

• G. Longo and L. Cardelli. A semantic basis for quest. Journal of Functional Programming, 1(4):417-458, 1991.

• Z. Luo. Computation and Reasoning -- A Type Theory for Computer Science, volume 11 of Monographs on Computer Science. Oxford University Press, 1994.

• Z. Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990. Available as report ECS-LFCS-90-118.

• Z. Luo. Program specification and data refinement in type theory. Mathematial Structures in Computer Science, 3, 1993.

• M. Makkai. The fibrational formulation of intuitionistic predicate logic. I: Completeness according to Gödel, Kripke, and Läuchli. Notre Dame Journal of Formal Logic, 34:334-377, 1993.

• M. Makkai and G.E. Reyes. First Order Categorical Logic, volume 611 of Lecture Notes in Mathematics. Springer-Verlag, Berlin, 1977.

• L.L. Maksimova, V.B. Shekhtman, and D.P. Skvortsov. The impossibility of a finite axiomatization of Medvedev's logic of finitary problems (Russian). Doklady, 245:1051-1054, 1979. Translation SM 20, pp. 394-398.

• P. Martin-Löf. Constructive mathematics and computer programming. In L.J. Cohen, J. Los, H. Pfeiffer, and K.-P. Podewski, editors, LMPS 6, pages 153-175. North-Holland, 1982.

• P. Martin-Löf. Intuitionistic Type Theory. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980. Bibliopolis, Napoli, 1984.

• P. Martin-Löf. An intuitionisitc theory of types, predicative part. In Logic Colloquium 1973, pages 73-118, 1975.

• D.C. McCarty. Information systems, continuity and realizability. In E. Clarke and D. Kozen, editors, Logics of Programs, volume 164 of Lecture Notes in Computer Science, pages 341-359. Springer, 1984.

• D.C. McCarty. Information systems, continuity and realizability. In E. Clarke and D. Cozen, editors, Logics of Programs, volume 164 of Lecture Notes in Computer Science. Springer-Verlag, 1984.

• D.C. McCarty. Markov's principle, isols and Dedekind finite sets. Journal of Symbolic Logic, 53:1042-1069, 1988.

• D.C. McCarty. Polymorphism and apartness. The Notre Dame Journal of Formal Logic, 32:513-532, 1991.

• D.C. McCarty. Realizability and Recursive Mathematics. D.Phil. Thesis, University of Oxford, 1984.

• D.C. McCarty. Realizability and recursive mathematics. Technical Report CMU-CS-84-131, Department of Computer Science, Carnegie-Mellon University, 1984. Report version of the author's PhD thesis, Oxford University 1983.

• D.C. McCarty. Subcountability under realizability. The Notre Dame Journal of Formal Logic, 27:210-220, 1986.

• C. McLarty. Elementary Categories, Elementary Toposes. Clarendon Press, 1995.

• Yu.T. Medvedev. Finite problems (Russian). Doklady, 142:1015-1018, 1962. Translation SM 3, pp. 227-230.

• Yu.T. Medvedev. An interpretation of intuitionistic number theory. In P. Suppes, G.C. Moisil, and A. Joja, editors, LMPS 4, pages 129-136. North-Holland, 1973.

• Yu.T. Medvedev. Interpretation of logical formulae by means of finite problems and its relation to the realizability theory (Russian). Doklady, 148:771-774, 1963. Translation SM 4, pp. 180-183.

• Yu.T. Medvedev. Interpretation of logical formulae by means of finite problems (Russian). Doklady, 169:20-23, 1966. Translation SM 7, pp. 857-860.

• Yu.T. Medvedev. Locally finitary algorithmic problems (Russian). Doklady, 203:285-288, 1972. Errata Ibidem 204, pp. 1286. Translation SM 13, pp. 382-386.

• Yu.T. Medvedev. A method for proving the unsolvability of algorithmic problems (Russian). Doklady, 185:1232-1235, 1969. Translation SM 10, pp. 495-498.

• R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, 1990.

• G.E. Mints. The completeness of provable realizability. The Notre Dame Journal of Formal Logic, 30:420-441, 1989.

• J.C. Mitchell. Foundations of Programming Languages. MIT Press, 1996.

• E. Moggi. Partial morphisms in categories of effective objects. Information and Computation, 76, 1988.

• J.R. Moschovakis. A classical view of the intuitionistic continuum. Annals of Pure and Applied Logic, 81:9-24, 1996.

• J.R. Moschovakis. A disjunctive decomposition theorem for classical theories. In F. Richman, editor, Constructive Mathematics, pages 250-259. Springer, 1981.

• J.R. Moschovakis. Disjunction and existence in formalized intuitionistic analysis. In J.N. Crossley, editor, Sets, Models, and Recursion Theory, pages 309-331. North-Holland, 1967.

• J.R. Moschovakis. An intuitionistic theory of lawlike, choice and lawless sequences. In Logic Colloquium '90, pages 191-209. Springer, 1993. (Lecture Notes in Logic 2).

• J.R. Moschovakis. Kleene's realizability and ``divides'' notions for formalized intuitionistic mathematics. In K.J. Barwise, H.J. Keisler, and K. Kunen, editors, The Kleene Symposium, pages 167-179. North-Holland, 1980.

• J.R. Moschovakis. Can there be no nonrecursive functions?. Journal of Symbolic Logic, 36:309-315, 1971.

• J.R. Moschovakis. More about relatively lawless sequences. Journal of Symbolic Logic, 59:813-829, 1994.

• J.R. Moschovakis. A topological interpretation of second-order intuitionistic arithmetic. Compositio Mathematica, 26:261-275, 1973.

• P. Mulry. Generalized Banach-Mazur functionals in the topos of recursive sets. Journal of Pure and Applied Algebra, 26:71-83, 1982.

• J.R. Myhill. Constructive set theory. Journal of Symbolic Logic, 40:347-382, 1975.

• J.R. Myhill. A note on indicator-functions. Proceedings of the American Mathematical Society, 29:181-183, 1973.

• J.R. Myhill. Some properties of intuitionistic Zermelo-Fraenkel set theory. In A.R.D. Mathias and H. Rogers, editors, Cambridge Summer School in Mathematical Logic, pages 206-231. Springer, 1973.

• D. Nelson. Recursive functions and intuitionistic number theory. Transactions of the American Mathematical Society, 61:307-368,556, 1947.

• B. Nordström, K. Petersson, and J.M. Smith. Programming in Martin Löf's Type Theory, volume 7 of Monographs on Computer Science. Oxford University Press, 1990.

• J. van Oosten and A.K. Simpson. Axioms and (counter)examples in synthetic domain theory. Technical Report 1080, Department of Mathematics, Utrecht University, 1998.

• J. van Oosten. Axiomatizing higher-order Kleene realizability. Annals of Pure and Applied Logic, 70:87-111, 1994.

• J. van Oosten. A combinatory algebra for sequential functionals of finite type. In S.B. Cooper and J.K. Truss, editors, Models and Computability, pages 389-406. Cambridge University Press, 1999.

• J. van Oosten. A combinatory algebra for sequential functionals of finite type. Technical Report 996, University of Utrecht, 1997.

• J. van Oosten. Exercises in Realizability. PhD thesis, Universiteit van Amsterdam, 1991.

• J. van Oosten. Extension of Lifschitz' realizability to higher order arithmetic, and a solution to a problem of F. Richman. Journal of Symbolic Logic, 56:964-973, 1991.

• J. van Oosten. Extensional realizability. Annals of Pure and Applied Logic, 84:317-349, 1997.

• J. van Oosten. Lifschitz' realizability. Journal of Symbolic Logic, 55:805-821, 1990.

• J. van Oosten. The modified realizability topos. Journal of Pure and Applied Algebra, 116:273-289, 1997.

• J. van Oosten. Two remarks on the Lifschitz realizability topos. Journal of Symbolic Logic, 61:70-79, 1996.

• J. van Oosten. A semantical proof of De Jongh's theorem. Archive for Mathematical Logic, pages 105-114, 1991.

• W.K.-S. Phoa. Building domains from graph models. Mathematical Structures in Computer Science, 2, 1992.

• W. Phoa. Domain Theory in Realizability Toposes. PhD thesis, Cambridge University, 1990.

• W. Phoa. Effective domains and intrinsic structure. In J. Mitchell, editor, Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science, pages 366-377, Philadelphia, Pennsylvania, 1990. IEEE Computer Society Press.

• W.K.-S. Phoa. An introduction to fibrations, topos theory, the effective topos and modest sets. Technical Report ECS-LFCS-92-208, Department of Computer Science, University of Edinburgh, 1992.

• W.K.-S. Phoa. Relative computability in the effective topos. Math. Proc. Camb. Phil. Soc, 106, 1989.

• W. Phoa. Relative computability in the effective topos. Mathematical Proceedings of the Cambridge Philosophical Society, 106:419-420, 1989.

• W.K.-S. Phoa. From term models to domains. In Proceedings of Theoretical Aspects of Computer Software, Sendai. Springer LNCS 526, 1991.

• A.M. Pitts. Categorical logic. Technical Report 367, University of Cambridge Computer Laboratory, 1995. To appear as a chapter of Handbook of Logic in Computer Science, Vol. V (Oxford University Press).

• A.M. Pitts. Conceptual completeness for first order intuitionistic logic: an application of categorical logic. Annals Pure Applied Logic, 41:33-81, 1989.

• A.M. Pitts. On an interpretation of second order quantification in first order intuitionistic propositional logic. Jour. Symbolic Logic, 57:33-52, 1992.

• A.M. Pitts. The Theory of Triposes. PhD thesis, Cambridge University, 1981.

• V.E. Plisko. Absolute realizability of predicate formulas (Russian). Izv. Akad. Nauk., 47:315-334, 1983. Translation Math. Izv. 22, pp. 291-308.

• V.E. Plisko. On the concept of relatively uniform realizability of propositional formulas (Russian). Vestnik Moskovskogo Universiteta Seriya I. Mathematika, Mekhanika, pages 77-79, 1992. Translated in Moscow University Mathematics Bulletin 47 (1992), 41-42.

• V.E. Plisko. A certain formal system that is connected with realizability (Russian). In B.A. Kushner and N.M. Nagornyi, editors, Teoriya Algorifmov i Matematicheskaya Logika: Sbornik Statej (Theory of Algorithms and Mathematical Logic. Collection of articles dedicated to Andrej Andrejevich Markov), pages 148-158,215. Vychislitel'nyj Tsentr Akademii Nauk SSSR, 1974.

• V.E. Plisko. On interpretations of predicate formulae that are connected with constructive logic (Russian). In 3 Vsesoyuznaya Konferentsiya po Matematicheskoj Logike. Tezitsy Doklady i Soobshcheniya (3rd All-Union Conference on Mathematical Logic), pages 170-172, 1974.

• V.E. Plisko. The nonarithmeticity of the class of realizable predicate formulas (Russian). Izv. Akad. Nauk., 41:483-502, 1977. Translation Math. Izv. 11, pp. 453-471.

• V.E. Plisko. On realizable predicate formulae (Russian). Doklady, 212:553-556, 1973. Translation SM 14, pp. 1420-1424.

• V.E. Plisko. Recursive realizability and constructive predicate logic (Russian). Doklady, 214:520-523, 1974. Translation SM 15, pp. 193-197.

• V.E. Plisko. Some variants of the notion of realizability for predicate formulas (Russian). Doklady, 226:61-64, 1976. Translation SM 17, pp. 59-63.

• V.E. Plisko. Some variants of the notion of realizability for predicate formulas (Russian). Izv. Akad. Nauk., 42:637-653, 1978. Translation Math. Izv. 12, pp. 588-604.

• M.B. Pour-El and J.I. Richards. Computability in Analysis and Physics. Springer-Verlag, 1989.

• M. Proietti. Connections between partial maps categories and tripos theory. In Category Theory and Computer Science (Edinburgh, 1987), volume 283 of Lecture Notes in Computer Science, pages 254-269. Springer-Verlag, Berlin, 1987.

• G.R. Renardel de Lavalette. Extended bar induction in applicative theories. Annals of Pure and Applied Logic, 50:139-189, 1990.

• G.R. Renardel de Lavalette. Theories with Type-free Application and Extended Bar Induction. PhD thesis, Universiteit van Amsterdam, 1984.

• B. Reus. Extensional Sigma -spaces in type theory. Applied Categorical Structures, 1999. To Appear.

• B. Reus and T. Streicher. General synthetic domain theory--a logical approach. Mathematical Structures in Computer Science, 9:177-223, 1999.

• B. Reus. Program Verification in Synthetic Domain Theory. Dokt.Diss., Lüdwig-Maximilians-Universität München, 1995. Shaker Verlag, Aachen.

• B. Reus. Synthetic domain theory in type theory: Another logic of computable functions. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96, volume 1125 of Lecture Notes in Computer Science, pages 363-381. Springer, 1996.

• E.P. Robinson and G. Rosolini. Colimit completions and the effective topos. Journal of Symbolic Logic, 55:678-699, 1990.

• E.P. Robinson. How complete is PER?. In A.R. Meyer, editor, Proceedings of the 4th Annual IEEE Symposium on Logic in Computer Science, pages 106-111, Asilomar, 1989. IEEE Computer Society Press.

• T.T. Robinson. Interpretations of Kleene's metamathematical predicate Gamma mid A in intuitionistic arithmetic. Journal of Symbolic Logic, 30:140-154, 1965.

• G.F. Rose. Propositional calculus and realizibility. Transactions of the American Mathematical Society, 75:1-19, 1953.

• J. Rosicky. Cartesian closed exact completions. Available from the Hypatia Electronic Library: http://hypatia.dcs.qmw.ac.uk, 1997.

• G. Rosolini. About modest sets. International Journal of Foundations of Computer Science, 1:341-353, 1990.

• G. Rosolini. Categories and effective computations. In D.H. Pitt, A. Poigné, and D.E. Rydeheard, editors, Category Theory and Computer Science, volume 283 of Lectures Notes in Computer Science, pages 1-11, Edinburgh, 1987. Springer-Verlag.

• G. Rosolini. Continuity and Effectiveness in Topoi. PhD thesis, University of Oxford, 1986.

• G. Rosolini. An ExPer model for Quest. In S. Brookes, M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, MFPS'91, volume 598 of Lecture Notes in Computer Science, pages 436-445. Springer, 1991.

• B. Scarpellini. A model for intuitionistic analysis. Commentarii Mathematici Helvetici, 45:440-471, 1970.

• B. Scarpellini. A new realizability notion for intuitionistic analysis. ZLGM, 23:137-167, 1977.

• A. Scedrov. Differential equations in constructive analysis and in the recursive realizability topos. Journal of Pure and Applied Algebra, 33:69-80, 1984.

• A. Scedrov and P. J. Scott. A note on the Friedman slash and Freyd covers. In A.S. Troelstra and D. van Dalen, editors, The L.E.J. Brouwer Centenary Symposium, pages 443-452. North-Holland, 1982.

• A. Scedrov. On the impossibility of explicit upper bounds on lengths of some provably finite algorithms in computable analysis. Annals of Pure and Applied Logic, 32:291-297, 1986.

• A. Scedrov. Recursive realizability semantics for Calculus of Constructions. Preliminary report. In G. Huet, editor, Logical Foundations of Functional Programming, pages 419-430. Addison-Wesley Publishing Company, 1990.

• A. Scedrov and R.E. Vesley. On a weakening of Markov's principle. Archiv, 23:153-160, 1983.

• D.S. Scott. Church's thesis and a unification of types, 1986.

• D.S. Scott. Data types as lattices. SIAM Journal of Computing, 5(3):522-587, 1976.

• D.S. Scott. Extending the topological interpretation to intuitionistic analysis. Compositio Mathematica, 20:194-210, 1968.

• D.S. Scott. A new category? Domains, spaces and equivalence relations. Manuscript, 1996.

• D.S. Scott. Relating theories of the lambda -calculus. In R. Hindley and J. Seldin, editors, To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalisms, pages 403-450. Academic Press, 1980.

• D.S. Scott, S. Awodey, A. Bauer, L. Birkedal, and J. Hughes. Logics of Types and Computation at Carnegie Mellon University. newline http://www.cs.cmu.edu/Groups/LTC/.

• P. Scowcroft. The disjunction and numerical existence properties for intuitionistic analysis. In J.N. Crossley, J.B. Remmel, R.A. Shore, and M.E. Sweedler, editors, Logical Methods, pages 747-781. Birkhaüser Boston, Inc., Boston MA, 1993.

• N.A. Shanin. Über einen Algorithmus zur konstruktiven Dechiffrierung mathematischer Urteile (Russian) (German summary). ZLGM, 4:293-303, 1958.

• N.A. Shanin. Concerning the constructive interpretation of auxiliary formulas I (Russian). Trudy Ordena Lenina Matematicheskogo Instituta imeni V. A. Steklova. Akademiya Nauk SSSR, 72:348-379, 1964. Translation AMS Transl. 99, pp. 233-275.

• N.A. Shanin. On the constructive interpretation of mathematical judgements (Russian). Trudy Ordena Lenina Matematicheskogo Instituta imeni V. A. Steklova. Akademiya Nauk SSSR, 52:226-311, 1958. Translation AMS Transl. 23, pp. 108-189.

• J.M. Smith. An interpretation of Kleene's slash in type theory. In G. Huet and G. Plotkin, editors, Logical Environments, pages 189-197, 1993.

• J. Staples. Combinator realizability of constructive finite type analysis. In A.R.D. Mathias and H. Rogers, editors, Cambridge Summer School in Mathematical Logic, pages 253-273. Springer, 1973.

• J. Staples. Combinator realizability of constructive Morse theory. Journal of Symbolic Logic, 39:226-234, 1974.

• M. Stein. A general theorem on existence theorems. ZLGM, 27:435-452, 1981.

• M. Stein. Interpretations of Heyting's arithmetic -- An analysis by means of a language with set symbols. AML, 19:1-31, 1980.

• M. Stein. Interpretationen der Heyting--Arithmetik endlicher Typen. Archiv, 19:175-189, 1979.

• T. Strahm. Partial applicative theories and explicit substitutions. Technical Report IAM 93-008, Institut für Informatik und angewandte Mathematik, Universität Bern, 1993.

• T. Streicher. Dependence and independece results for (impredicative) calculi of dependent types. Mathematical Structures in Computer Science, 2:29-54, 1992.

• T. Streicher. Independence of the induction principle and the axiom of choice in the pure calculus of constructions. Theoretical Computer Science, 103:395-408, 1992.

• T. Streicher. Investigations into intensional type theory. Habilitationsschrift, Universität München, 1994.

• T. Streicher. Mathematical independencies in the pure calculus of constructions. Technical Report MIP-909, Fakultät für Mathematik und Informatik, Universität Passau, 1991.

• T. Streicher. Semantics of Type Theory, Correctness, Completeness and Independence Results. Birkhäuser, 1991.

• M.D.G. Swaen. A Characterization of ML in Many-Sorted Arithmetic with Conditional Application. Journal of Symbolic Logic, 57:924-953, 1992.

• M.D.G. Swaen. The logic of first-order intuitionistic type theory with weak sigma-elimination. Journal of Symbolic Logic, 56:467-483, 1991.

• M.D.G. Swaen. Weak and Strong Sum-Elimination in Intuitionistic Type Theory. PhD thesis, Universiteit van Amsterdam, 1989.

• W.W. Tait. A realizability interpretation of the theory of species. In R.J. Parikh, editor, Logic Colloquium, pages 240-251. Springer, 1975.

• W.W. Tait. A realizability interpretation of the theory of species. In R. Parikh, editor, Logic Colloquium, volume 453 of Lectures Notes in Mathematics, pages 240-251, Boston, 1975. Springer-Verlag.

• M. Tatsuta. Monotone recursive definition of predicates and its realizability interpretation. In Proceedings of Theoretical Aspects of Computer Software, pages 38-52. Springer, 1991.

• M. Tatsuta. Program synthesis using realizability. Theoretical Computer Science, 90:309-353, 1991.

• M. Tatsuta. Realizability interpretation of coinductive definitions and program synthesis with streams. In Proceedings of International Conference on Fifth Generation Computer Systems, pages 666-673, 1992.

• P. Taylor. The fixed point property in synthetic domain theory. In 6th Symp. on Logic in Computer Science, pages 152-160. IEEE Computer Society Press, 1991.

• L.H. Tharp. A quasi-intuitionistic set theory. Journal of Symbolic Logic, 36:456-460, 1971.

• R.R. Tompkins. On Kleene's recursive realizability as an interpretation for intuitionistic elementary number theory. Notre Dame Journal of Formal Logic, 9:289-293, 1968.

• A.S. Troelstra. Axioms for intuitionistic mathematics incompatible with classical logic. In R.E. Butts and J. Hintikka, editors, LMPS 5, volume 1, pages 59-84. D. Reidel, Dordrecht and Boston, 1977.

• A.S. Troelstra. Computability of terms and notions of realizability for intuitionistic analysis. Technical Report 71-02, Department of Mathematics, University of Amsterdam, 1971.

• A.S. Troelstra. Comparing the theory of representations and constructive mathematics. In E. Börger, G. Jäger, H. Kleine Büning, and M.M. Richter, editors, Computer Science Logic. 5th workshop, CSL '91, pages 382-395. Springer, 1992.

• A.S. Troelstra and D. van Dalen. Constructivism in Mathematics. North-Holland, 1988. 2 volumes.

• A.S. Troelstra. Extended bar induction of type zero. In K.J. Barwise, H.J. Keisler, and K. Kunen, editors, The Kleene Symposium, pages 277-316. North-Holland, 1980.

• A.S. Troelstra. Notes on intuitionistic second order arithmetic. In A.R.D. Mathias and H. Rogers, editors, Cambridge Summer School in Mathematical Logic, pages 171-205. Springer, 1973.

• A.S. Troelstra, editor. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Springer, 1973. With contributions by A.S. Troelstra, C.A. Smorynski, J.I. Zucker and W.A. Howard.

• A.S. Troelstra. Some models for intuitionistic finite type arithmetic with fan functional. Journal of Symbolic Logic, 42:194-202, 1977.

• A.S. Troelstra. A note on non-extensional operations in connection with continuity and recursiveness. Indagationes Mathematicae, 39:455-462, 1977.

• A.S. Troelstra. Notions of realizability for intuitionistic arithmetic and intuitionistic arithmetic in all finite types. In J.E. Fenstad, editor, The Second Scandinavian Logic Symposium, pages 369-405. North-Holland, 1971.

• A.S. Troelstra. Realizability. In S.R. Buss, editor, Handbook of Proof Theory, pages 407-473. North-Holland, 1998.

• G. S. Tsejtin. The disjunctive rank of the formulas of constructive arithmetic (Russian). Zapiski, 8:260-271, 1968. Translation Seminars in Mathematics. V.A.Steklov Mathematical Institute Leningrad 8(1970), pp. 126-132. This volume appeared as: A.O. Slisenko (ed.), Studies in Constructive Mathematics and Mathematical Logic. Part II. Consultants Bureau, New York, London.

• D. van Dalen and A.S. Troelstra. Constructivism in Mathematics. North Holland Publishing Company, 1988.

• F.L. Varpahovskij. A class of realizable propositional formulas. Zapiski, 1:8-23, 1971. Translation Journal of Soviet Mathematics 1,1-11 (1973).

• R.E. Vesley. A palatable substitute for Kripke's schema. In A. Kino, J.R. Myhill, and R.E. Vesley, editors, Intuitionism and Proof Theory, pages 197-207. North-Holland, 1970.

• R.E. Vesley. Realizing Brouwer's sequences. Annals of Pure and Applied Logic, 81:25-74, 1996.

• A. Voronkov. On completeness of program synthesis systems. In E. Börger, G. Jäger, H. Kleine Büning, and M.M. Richter, editors, Computer Science Logic. 5th workshop, CSL '91, pages 411-418. Springer, 1992.

• A. Voronkov. N-realizability: one more constructive semantics. Technical Report 71, Department of Mathematics, Monash University, Australia, 1991.

• K.F. Wehmeier. Fragments of HA based on Sigma ₁-induction, 1996. Preprint. Part of the author's dissertation project at the University of Münster, Westphalia, Germany.