Foundations and logical aspects of constructivism

Aczel, P.: The strength of Martin-Löf's intuitionistic type theory with one universe. In: S. Miettinen and J. Väänänen (eds.), Proc. Symp. on Mathematical Logic (Oulo 1974), Report no. 2, Dept. of Philosophy, Univ. of Helsinki, 1977.

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

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

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

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

Beeson, M.: Continuity in intuitionistic set theories. In: M. Boffa et al. (eds.), Logic Colloquium '78, (North-Holland, Amsterdam 1979), 1 - 52.

Beeson, M.: Extensionality and choice in constructive mathematics. Pac. J. Math. 88(1980), 1 - 28.

Beeson, M.: Problematic Principles in Constructive Mathematics. In: D. van Dalen et al. (eds.), Logic Colloquium '80, (North-Holland, Amsterdam 1982), 11 - 55.

Beeson, M.: Recursive models for constructive set theories. Ann. Math. Logic 23(1982), 127-178.

Beeson, M.: Foundations of Constructive Mathematics. (Springer, Berlin Heidelberg New York 1985).

Beeson, M.: Proving programs and programming proofs. In: R. Barcan Marcus et al. (eds.) Proc. of the Seventh International Conference on Logic, Mathodology and Philosophy of Science, (Elsevier, Amsterdam 1986), 51-82.

Beeson, M.: Some theories conservative over intuitionistic arithmetic. In: Comtemporary Mathematics, vol 106, (American Math. Soc. 1990), 1-15.

Bishop, E.: Mathematics as a numerical language. In: Intuitionism and Proof Theory, (North-Holland, Amsterdam 1970), 53-71.

Bishop, E.: The Crisis in Contemporary Mathematics. Historia Math., 2(1975), 507 - 517.

Bishop, E.: Schizophrenia in Contemporary Mathematics. In: Contemporary Mathematics, vol 39, American Mathematical Society 1985.

Bishop, E.: Compiling Mathematics into Algol. Unpublished manuscript.

Bridges, D.S.: Towards a constructive foundation for quantum mechanics. In: F. Richman (ed.) Constructive Mathematics, Lecture Notes in Mathematics, vol. 873, (Springer 1981) 260 - 273.

Bridges, D.S., Richman, F.: Varieties of Constructive Mathematics. London Mathematical Society Lecture Notes, vol. 97, Cambridge University Press, 1987.

Dalen, D. van: Braucht die konstruktive Mathematik Grundlagen. Jber. Deutsche Math.-Verein. 84(1982), 57-78.

Dragalin, A.G.: Mathematical Intuitionism: Introduction to Proof Theory. (Translations of mathematical monographs) American Mathematical Society 1988.

Dummett, M.: Elements of Intuitionism. Clarendon Press, Oxford 1977.

Feferman, S.: Iterated inductive fixed-point theories: application to Hancock's conjecture. In: G. Metakides (ed.) Patras Logic Symposium, North-Holland, Amsterdam, 1982.

Friedman, H.: Set Theoretic Foundations for Constructive Analysis. Ann. of Math. 105(1977), 1 -- 28.

Goodman, N.D., Myhill, J.: The formalization of Bishop's constructive mathematics. In: F.W. Lawvere (ed.), Toposes, Algebraic Geometry and Logic, Lecture Notes in Mathematics, vol. 274, Springer, Berlin Heidelberg New York, 1972.

Griffor, E. , Rathjen, M.: The strength of some Martin-Löf's type theories. Archive for Mathematical Logic 33(1994). 347 - 385.

Gurevich, Yu.: Platonism, Constructivism and Computer Proofs vs. Proofs by Hand. Bulletin of EATCS, October 1995.

Hellman, G.: Constructive mathematics and quantum mechanics: unbounded operators and the spectral theorem. J. Philosophical Logic 22(1993), 221-248.

Heyting, A.: Intuitionism. (North-Holland, Amsterdam 1956).

Kleene, S.C., Vesley, R.E.: The Foundations of Intuitionistic Mathematics. North-Holland, Amsterdam 1965.

Martin-Löf, P.: Notes on Constructive Mathematics. (Almqvist och Wiksell, Stockholm 1970).

Martin-Löf, P.: Infinite terms and a system of natural deduction. Compositio Mathematica, 24(1972), 93 -103.

Martin-Löf, P. Hauptsatz for the intuitionistic theory of of iterated inductive definitions. In: J.E. Fenstad (ed.), Proceedings of the Second Scandinavian Logic Symposium, (North-Holland, Amsterdam 1971) 179 - 216.

Martin-Löf, P.: About models for intuitionistic type theories and the notion of definitional equality. In: S. Kanger (ed.) Proceedings of the Third Scandinavian Logic Symposium, (North-Holland, Amsterdam) 81 - 109.

Martin-Löf, P.: An intuitionistic theory of types: predicative part. In: H.E. Rose and J. Shepherdson (eds.) Logic Colloquium '73, North-Holland, Amsterdam, 1975.

Martin-Löf, P.: Constructive mathematics and computer programming. in: L.J. Cohen et al. (eds.), Logic, Methodology and Philosophy of Science VI, North-Holland, Amsterdam, 1982.

Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis, 1984.

Martin-Löf, P.: Truth of a proposition, evidence of a judgement, validity of a proof. Synthese 73(1987), 407 - 420.

Martin-Löf, P.: Analytic and synthetic judgements in type theory. In: P. Parrini (ed.), Kant and Contemporary Esistemology, (Kluwer, Dordrecht 1994), 87 - 99.

Martin-Löf, P.: On the meanings of the logical constants and the justifications of the logical laws. Nordic Journal of Philosophical Logic 1(1996), 11 - 60.

Myhill, J.: Constructive Set Theory. J. Symbolic Logic, 40(1975), 347-382.

Nordström, P., Peterson, K., Smith, J.M.: Programming in Martin-Löf's Type Theory. Oxford University Press, 1990.

Palmgren, E.: Type-theoretic interpretation of strictly positive, iterated inductive definitions. Archive for Mathematical Logic 32(1992), 75 -- 99.

Richman, F.: Meaning and information in constructive mathematics. American Mathematical Society, 89(1982), 385 - 388.

Setzer, A.: Proof Theoretical Strength of Martin-Löf Type Theory with W-type and one Universe. Dissertation Munich, 1993.

Setzer, A.: A type theory for one Mahlo universe. Manuscript, September 1995.

Schwichtenberg, H.: A normal form for natural deductions in a type theory with realizing terms. In: Atti del Congresso Logica e Filosofia della Scienza, oggi., San Gimignano, 7-11 dicembre 1983, Vol I - Logica, CLUEB, Bologna, 1986.

Smith, J.M.: The independence of Peano's fourth axiom from Martin-Löf's type theory without universes. J. Symbolic Logic 53(1988), 840--845.

Stewart, I.: Frog and mouse revisited: a review of Constructive Analysis by E. Bshop and D.S. Bridges and An Introdction to Nonstandard Real Analysis by A.E. Hurd and P. Loeb. Mathematical Intelligencer 8(1986), 78 - 82.

Troelstra, A.S.: Principles of Intuitionism. Lecture Notes in Mathematics, vol. 95, Springer, Berlin, 1969.

Troelstra, A.S. (ed.): Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics, vol. 344, Springer, Berlin Heidelberg New York, 1973.

Troelstra, A.S.: Note on the fan theorem. J. Symbolic Logic 39(1974), 584 - 596.

Troelstra, A. S., Dalen, D. van: Constructivism in mathematics: An introduction. Volume I and II. Amsterdam: North-Holland 1988.

Weyl, H.; Das Kontinuum. Kritische Untersuchungen über die Grundlagen der Analysis. Veit, Leipzig 1918.

Weyl, H.: Über die Neue Grundlagenkrise der Mathematik. Mathematische Zeitschrift, 10 (1921), 39 -- 79.