Linked bibliography for the SEP article "Type Theory" by Thierry Coquand

This is an automatically generated and experimental page

If everything goes well, this page should display the bibliography of the aforementioned article as it appears in the Stanford Encyclopedia of Philosophy, but with links added to PhilPapers records and Google Scholar for your convenience. Some bibliographies are not going to be represented correctly or fully up to date. In general, bibliographies of recent works are going to be much better linked than bibliographies of primary literature and older works. Entries with PhilPapers records have links on their titles. A green link indicates that the item is available online at least partially.

This experiment has been authorized by the editors of the Stanford Encyclopedia of Philosophy. The original article and bibliography can be found here.

  • Aczel, P., 1978, “The type theoretic interpretation of constructive set theory”, Logic Colloquium '77, Amsterdam: North-Holland, 55–66. (Scholar)
  • Andrews, P., 2002, An introduction to mathematical logic and type theory: to truth through proof (Applied Logic Series: Volume 27), Dordrecht: Kluwer Academic Publishers, second edition. (Scholar)
  • Awodey, S., Pelayo, A., Warren, M. 2013, “The Axiom of Univalence in Homotopy Type Theory”, Notices of the American Mathematical Society, 60(09): 1157–1164. (Scholar)
  • Barendregt, H., 1997, “The impact of the lambda calculus in logic and computer science”, Bulletin of Symbolic Logic, 3(2): 181–215. (Scholar)
  • –––, 1992, Lambda calculi with types. Handbook of logic in computer science, Volume 2, Oxford, New York: Oxford University Press, 117–309. (Scholar)
  • Bell, J.L. 2012, “Types, Sets and Categories”, in Akihiro Kanamory Handbook of the History of Logic. Volume 6: Sets and Extensions in the Twentieth Century, Amsterdam: North Holland. (Scholar)
  • Bourbaki, N., 1958, Théorie des Ensembles, 3rd edition, Paris: Hermann. (Scholar)
  • de Bruijn, N. G., 1980, “A survey of the project AUTOMATH”, in To H. B. Curry: essays on combinatory logic, lambda calculus and formalism, London-New York: Academic Press, 579–606.
  • Burgess J. P. and Hazen A. P., 1998, “Predicative Logic and Formal Arithmetic Source,” Notre Dame J. Formal Logic, 39(1): 1–17. (Scholar)
  • Buchholz, W. Schütte, 1988, Proof theory of impredicative subsystems of analysis. Studies in Proof Theory, Monographs 2, Naples: Bibliopolis. (Scholar)
  • Church, A., 1940, “A formulation of the simple theory of types,” J Symbolic Logic, 5: 56–68
  • –––, 1984, “Russell's theory of identity of propositions,” Philosophia Naturalis, 21: 513–522 (Scholar)
  • Chwistek, L., 1948, The Limits of Science: Outline of Logic and of the Methodology of the Exact Sciences, London: Routledge and Kegan Paul. (Scholar)
  • Coquand, T., 1986, “An analysis of Girard's paradox,” Proceedings of the IEEE Symposium on Logic in Computer Science, 227–236. (Scholar)
  • –––, 1994, “A new paradox in type theory,” Stud. Logic Found. Math. (Volume 134), Amsterdam: North-Holland, 555–570.
  • du Bois-Reymond, P., 1875, “Ueber asymptotische Werthe, infintaere Appproximationen und infitaere Aufloesung von Gleichungen,” Mathematische Annalen, 8: 363–414. (Scholar)
  • Feferman, S., 1964, “Systems of predicative analysis,” Journal of Symbolic Logic, 29: 1–30. (Scholar)
  • Ferreira, F. and Wehmeier, K., 2002, “On the consistency of the Delta-1-1-CA fragment of Frege's Grundgesetze,” Journal of Philosophic Logic, 31: 301–311. (Scholar)
  • Girard, J.Y., 1972, Interpretation fonctionelle et eleimination des coupures dans l'arithmetique d'ordre superieure, These d'Etat, Université Paris 7. (Scholar)
  • Gödel, K., 1995, Collected Works Volume III, Unpublished Essays and Lectures, Oxford: Oxford University Press, 1995. (Scholar)
  • –––, 1931, “Uber formal untentschedibare Saetze der Principia Mathematica und verwandter Systeme I,” Monatsh. Math. Phys, 38: 349–360. (Scholar)
  • –––, 1944, “Russell's mathematical logic,” in The philosophy of Bertrand Russell, P. A. Schilpp (ed.), Evanston: Northwestern University Press, 123–153. (Scholar)
  • –––, 1958, “Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes,”, Dialectica, 12: 280–287. (Scholar)
  • Heck, Richard G., Jr, 1996, “The consistency of predicative fragments of Frege's Grundgesetze der Arithmetik,” History and Philosophy of Logic, 17 (4): 209–220. (Scholar)
  • van Heijenoort, 1967, From Frege to Gödel. A source book in mathematical logic 1879–1931, Cambridge, MA: Harvard University Press. (Scholar)
  • Hindley, R., 1997, Basic Simple Type Theory, Cambridge: Cambridge University Press. (Scholar)
  • Hofmann, M. and Streicher, Th. 1996, “The Groupoid interpretation of Type Theory,” in Twenty-five years of constructive type theory (Oxford Logic Guides: Volume 36), Oxford, New York: Oxford University Press, 83–111. (Scholar)
  • Howard, W. A., 1980, “The formulae-as-types notion of construction,” in To H. B. Curry: essays on combinatory logic, lambda calculus and formalism, London, New York: Academic Press, 480–490. (Scholar)
  • Hurkens, A. J. C., 1995, “A simplification of Girard's paradox. Typed lambda calculi and applications,” in Lecture Notes in Computer Science (Volume 902), Berlin: Springer: 266–278. (Scholar)
  • Lambek, J., 1980. “From λ-calculus to Cartesian Closed Categories” in To H.B. Curry: Essays on Combinatory Logic, λ-calculus and Formalism, J. Seldin and J. Hindley (eds.), London, New York: Academic Press. pp. 375–402. (Scholar)
  • Lambek, J. and Scott, P. J., 1986, Introduction to higher order categorical logic (Cambridge Studies in Advanced Mathematics: Volume 7), Cambridge: Cambridge University Press; reprinted 1988. (Scholar)
  • Lawvere, F. W. and Rosebrugh, R., 2003, Sets for mathematics, Cambridge: Cambridge University Press. (Scholar)
  • Martin-Löf, P., 1970, Notes on constructive mathematics, Stockholm: Almqvist & Wiksell. (Scholar)
  • –––, 1971, A Theory of Types, Preprint, Stockholm University. (Scholar)
  • –––, 1998, “An intuitionistic theory of types,” in Twenty-five years of constructive type theory (Oxford Logic Guides: Volume 36), Oxford, New York: Oxford University Press, 127–172. (Scholar)
  • –––, 1973, “An intuitionistic theory of types: Predicative Part,” in Logic Colloquium, 1973, North-Holland, volume 80, 73–118. (Scholar)
  • Myhill, J., 1974, “The Undefinability of the Set of Natural Numbers in the Ramified Principia”, in Bertrand Russell's Philosophy, G. Nakhnikian (ed.), London: Duckworth, 19–27. (Scholar)
  • Miquel, A., 2001, Le Calcul des Constructions implicite: syntaxe et sémantique, Thèse de doctorat, Université Paris 7. (Scholar)
  • –––, 2003, “A strongly normalising Curry-Howard correspondence for IZF set theory,” in Computer science Logic (Lecture Notes in Computer Science, 2803), Berlin: Springer: 441–454. (Scholar)
  • Oppenheimer, P. and E. Zalta, 2011, “Relations Versus Functions at the Foundations of Logic: Type-Theoretic Considerations”, Journal of Logic and Computation, 21: 351–374. (Scholar)
  • Palmgren, Erik, 1998, “On universes in type theory,” in Twenty-five years of constructive type theory (Oxford Logic Guides: Volume 36), Oxford, New York: Oxford University Press, 191–204. (Scholar)
  • Poincaré, 1909, “H. La logique de l'infini” Revue de metaphysique et de morale, 17: 461–482. (Scholar)
  • Prawitz, D., 1967, “Completeness and Hauptsatz for second order logic”, Theoria, 33: 246–258. (Scholar)
  • –––, 1970, “On the proof theory of mathematical analysis,” in Logic and value (Essays dedicated to Thorild Dahlquist on his fiftieth birthday), Filosofiska Studier, No. 9, Filosof. Föreningen och Filosof. Inst., Uppsala Univ., Uppsala, 169–180. (Scholar)
  • Quine, W., 1940, “Review of Church ‘A formulation of the simple theory of types’,” Journal of Symbolic Logic, 5: 114. (Scholar)
  • Ramsey, F.P., 1926, “The foundations of mathematics,” Proceedings of the London Mathematical Society, s2–25 (1), 338–384. (Scholar)
  • Russell, B., 1903, The Principles of Mathematics, Cambridge: Cambridge University Press. (Scholar)
  • –––, 1908, “Mathematical logic as based on the theory of types,” American Journal of Mathematics, 30: 222–262. (Scholar)
  • –––, 1959, My philosophical development, London and New York: Routledge. (Scholar)
  • Russell, B. and Whitehead, A., 1910, 1912, 1913, Principia Mathematica (3 volumes), Cambridge: Cambidge University Press. (Scholar)
  • Reynolds, J., 1974, “Towards a theory of type structure,” in Programming Symposium Lecture Notes in Computer Science (Volume 19), Berlin: Springer, 408–425. (Scholar)
  • –––, 1983, “Types, Abstraction and Parametric Polymorphism,” IFIP Congress, Paris, 513–523. (Scholar)
  • –––, 1984, “Polymorphism is not set-theoretic. Semantics of data types,” Lecture Notes in Computer Science (Volume 173), Berlin: Springer, 145–156. (Scholar)
  • –––, 1985, “Three approaches to type structure. Mathematical foundations of software development,” in Lecture Notes in Computer Science (Volume 185), Berlin: Springer, 97–138. (Scholar)
  • Schütte, K., 1960, Beweistheorie, Berlin: Springer-Verlag. (Scholar)
  • Scott, D., 1993 “A type-theoretic alternative to ISWIM, CUCH, OWHY,” Theoretical Computer Science, 121: 411–440.
  • Skolem, T., 1970, Selected works in logic, Jens Erik Fenstad (ed.), Oslo: Universitetsforlaget. (Scholar)
  • Tait, W. W., 1967, “Intensional interpretations of functionals of finite type,” Journal of Symbolic Logic, 32 (2): 198–212. (Scholar)
  • Takeuti, G., 1955 “On the fundamental conjecture of GLC: I”, J. Math. Soc. Japan, 7: 249–275. (Scholar)
  • –––, 1967, “Consistency proofs of subsystems of classical analysis,” The Annals of Mathematics (Second Series), 86 (2): 299–348. (Scholar)
  • Tarski, A., 1931, “Sur les ensembles definissables de nombres reels I,” Fund. Math., 17: 210–239. (Scholar)
  • The Univalent Foundations Program, 2013, Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study. (Scholar)
  • Urquhart, A., 2003, “The Theory of Types,” in The Cambridge Companion to Bertrand Russell, Nicholas Griffin (ed.), Cambridge: Cambridge University Press. (Scholar)
  • Voevodsky, V., 2009, Univalent Foundations of Mathematics, available online. (Scholar)
  • Wiener, N., 1914, “A simplification of the logic of relations,” Proceedings of the Cambridge Philosophical Society, 17: 387–390.
  • Weyl, H., 1946, “Mathematics and Logic,” American Mathematical Monthly, 53: 2–13. (Scholar)
  • Zermelo, E., 1908, “Untersuchungen über die Grundlagen der Mengenlehre I,” Mathematische Annalen, 65: 261–281. (Scholar)

Generated Thu May 25 07:08:40 2017