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. and Carus, A.W., 2001, “Carnap, completeness and categoricity: the Gabelbarkeitssatz of 1928”, Erkenntnis, 54: 145–171. (Scholar)
––– and Pelayo, A., Warren, M. 2013, “The Axiom of Univalence in Homotopy Type Theory”, Notices of the American Mathematical Society, 60(9): 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. and K. Schütte, 1988, Proof theory of impredicative subsystems of analysis (Studies in Proof Theory: Monograph 2), Naples: Bibliopolis. (Scholar)
Church, A., 1940, “A formulation of the simple theory of types,” Journal of Symbolic Logic, 5: 56–68
–––, 1984, “Russell’s theory of identity of propositions,” Philosophia Naturalis, 21: 513–522 (Scholar)
Chwistek, L., 1926, “Ueber die Hypothesen der Mengelehre,” Mathematische Zeitschrift, 25: 439–473 (Scholar)
–––, 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)
Fitch, F. B., 1964, “The hypothesis that infinite classes are similar,” Journal of Symbolic Logic, 4: 159–162. (Scholar)
Girard, J.Y., 1972, Interpretation fonctionelle et eleimination des coupures dans l’arithmetique d’ordre superieure, These d’Etat, Université Paris 7. (Scholar)
Goldfarb, Warren, 2005. “On Godel’s way in: The influence of Rudolf Carnap.” Bulletin of Symbolic Logic 11(2): 185–193. (Scholar)
Gödel, K., 1995, Collected Works Volume III, Unpublished Essays and Lectures, Oxford: Oxford University Press, 1995. (Scholar)
–––, 1931, “Über formal untentscheidbare Sätze der Principia Mathematica und verwandter Systeme I,” Monatshefte fü Mathematik und Physik, 38: 173–198. (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, R., 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)
Hodges, W., 2008, “Tarski on Padoa’s Method: a test case for understanding logicians of other traditions”, in Logic, Navya-Nyāya and Applications: Homage to Bimal Krishna Matilal, Mihir K. Chakraborti et al. (eds.), London: College Publications, pp. 155–169 (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 \(\lambda\)-calculus to Cartesian Closed Categories” in To H.B. Curry: Essays on Combinatory Logic, \(\lambda\)-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, Technical Report 71–3, Stockholm: 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)
–––, 1975 [1973], “An intuitionistic theory of types: Predicative Part,” in Logic Colloquium ’73 (Proceedings of the Logic Colloquium, Bristol 1973) (Studies in Logic and the Foundations of Mathematics: Volume 80), H.E. Rose and J.C. Shepherdson (eds.), Amsterdam: North-Holland, 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 (Filosof. Föreningen och Filosof. Inst.), No. 9, Uppsala: Uppsala University, 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., 1901, “Sur la logique des relations avec des applications a la théorie des séries”, Revue de Mathématique, 7: 115–136, 137–148. (Scholar)
–––, 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)
–––, 1919, Introduction to Mathematical Philosophy, London: George Allen and Unwin. (Scholar)
–––, 1959, My philosophical development, London, 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,” Proceedings of the IFIP 9th World Computer 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)
Schiemer, G. and Reck, E.H., 2013, “Logic in the 1930s: Type Theory and Model Theory,” The Bulletin of Symbolic Logic, 19(4): 433–472. (Scholar)
Schütte, K., 1960, Beweistheorie, Berlin: Springer-Verlag. (Scholar)
–––, 1960b, “Syntactical and Semantical Properties of Simple Type Theory,” Journal of Symbolic Logic, 25: 305–326. (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”, Journal of the Mathematical Society of 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,” Fundamenta Mathematicae, 17: 210–239. (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., 2015, “An experimental library of formalized mathematics based on univalent foundations,” Mathematical Structures in Computer Science, 25: 1278–1294, 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 Tue Dec 3 04:42:19 2024

Applied ethics	Epistemology	History of Western Philosophy	Meta-ethics	Metaphysics	Normative ethics
Philosophy of biology	Philosophy of language	Philosophy of mind	Philosophy of religion	Science Logic and Mathematics	More ...