The strength of some Martin-L�f type theories

[A 77] Aczel, P.: The strength of Martin-Löf's intuitionistic type theory with one universe. In: Miettinen, S., Vaänänen, S. (eds.) Proceedings of Symposia in Mathematical Logic. Oulu 1974, and Helsinki 1975. Report No. 2, University of Helsinki, Department of Philosophy, 1977, 1?32

[A 78] Aczel, P.: The type theoretic interpretation of constructive set theory. In: MacIntyre, A., Pacholski, L., Paris, J. (eds.) Logic Colloquium '77. Amsterdam: North-Holland 1978

[A 82] Aczel, P.: The type theoretic interpretation of constructive set theory: choice prinicples. In: Troelstra, A.S., van Dalen, D. (eds.) The L.E.J. Brouwer Centenary Symposium. Amsterdam: North-Holland 1982

[A 86] Aczel, P.: The type theoretic interpretation of constructive set theory: inductive definitions. In: Marcus, R.B. et al. (eds) Logic, Methodology, and Philosopy of Science VII. Amsterdam: North-Holland 1986

[Ba 75] Barwise, J.: Admissible sets and structures. Berlin: Springer 1975

[Be 82] Beeson, M.: Recursive models for constructive set theories. Ann. Math. Logic23, 126?178 (1982)

[Be 85] Beeson, M.: Foundations of constructive mathematics. Berlin: Springer 1985

[BFPS 81] Buchholz, W., Feferman, S., Pohlers, W., Sieg, W.: Iterated inductive definitions and subsystems of analysis. Lect. Notes Math. 897. Berlin: Springer 1981

[F 75] Feferman, S.: A language and axioms for explicit mathematics. Lect. Notes Math.450, 87?139 (1975)

[F 79] Feferman, S.: Constructive theories of functions and classes. In: Boffa, M., van Dalen, D., McAloon, K. (eds.) Logic Colloquium '78, pp.IARI 159?224. Amsterdam: North-Holland 1979

[FS 81] Feferman, S., Sieg, W.: Proof-theoretic equivalences between classical and constructive theories of analysis. Lect. Notes Math.897, 78?142 (1981)

[GP 90] Griffor, E.R., Palmgren, E.: An intuitionistic theory of transfinite types. Uppsala: University of Uppsala Preprint 1990

[J 82] Jäger, G.: Zur Beweistheorie der Kripke-Platek-Mengenlehre über den natürlichen Zahlen. Arch. Math. Logik22, 121?139 (1982)

[J 83] Jäger, G.: A well-ordering proof for Feferman's theoryT 0. Arch Math. Logik23, 65?77 (1983)

[JP 82] Jäger, G., Pohlers, W.: Eine beweistheoretische Untersuchung von? 2 1 ?CA +BI und verwandter Systeme. Sitzungsberichte der Bayerischen Akademie der Wissenschaften, Mathematisch-Naturwissenschaftliche Klasse (1982)

[ML 84] Martin-Löf, P.: Intuitionistic type theory. Naples:Bibliopolis 1984

[My 75] Myhill, J.: Constructive set theory. JSL40, 347?382 (1975)

[NPS 90] Nordström, B., Petersson, K., Smith, J.M.: Programming in Martin-Löf's type theory. Oxford: Clarendon Press, 1990

[P 93] Palmgren, E.: Type-theoretic interpretations of iterated, strictly positive inductive definitions. Arch. Math. Logic32, 75?99 (1993)

[R 89] Rathjen, M.: Untersuchungen zu Teilsystemen der Zahlentheorie zweiter Stufe und der Mengenlehre mit einer zwischen ? 2 1 ?CA und ? 2 1 ?CA+? 2 1 ?BI liegenden Beweisstärke. Münster: University of Münster, Institute for Mathematical Logic and Foundational Research 1989

[R 91] Rathjen, M.: Proof-theoretic analysis of KPM. Arch. Math. Logic30, 377?403 (1991)

[S 93] Setzer, T.: Proof theoretical strength of Martin-Löf type theory with W-type and one universe. Thesis, University of Munich, 1993

[TD 88] Troelstra, A. S., van Dalen, D.: Constructivism in mathematics: an introduction, vol.IARIume II. Amsterdam: North-Holland 1988