Linked bibliography for the SEP article "Intuitionistic Type Theory" by Peter Dybjer and Erik Palmgren

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, Peter, 1978 [1977], “The type theoretic interpretation of constructive set theory”, in Logic Colloquium ’77, A. Macintyre, L. Pacholski, J. Paris (eds), Amsterdam-New York: North-Holland, pp. 55–66. (Scholar)
–––, 1980, “Frege Structures and the Notions of Proposition, Truth and Set”, in The Kleene Symposium, J. Barwise, H.J. Keisler, K. Kunen (eds), Studies in Logic and the Foundations of Mathematics 101, Amsterdam: North-Holland, pp. 31–59. (Scholar)
Altenkirch, Thorsten, Simon Boulier, Ambrus Kaposi, Nicolas Tabareau, 2019, “Setoid type theory – a syntactic translation”, MPC 2019 – 13th International Conference on Mathematics of Program Construction, Oct 2019, Porto, Portugal. pp.155–196. (Scholar)
Asperti, Andrea, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi, 2011, “The Matita interactive theorem prover”, in Automated deduction: CADE-23, N. Bjørner and V. Sofronie-Stokkermans (eds), Lecture Notes in Computer Science (LNCS), vol. 6803, Heidelberg: Springer-Verlag, pp. 64–69. (Scholar)
Awodey, Steve and Michael A. Warren, 2009, “Homotopy theoretic models of identity types”, Mathematical Proceedings of the Cambridge Philosophical Society, 146(1): 45–55. (Scholar)
Beeson, Michael, 1985, Foundations of Constructive Mathematics, Springer-Verlag, Berlin. (Scholar)
van den Berg, Benno and Richard Garner, 2011, “Types are weak \(\omega\)-groupoids”, Proceedings of the London Mathematical Society, 102(2): 370–394. doi:10.1112/plms/pdq026 (Scholar)
Bezem, Marc, Thierry Coquand, and Simon Huber, 2014 [2013], “A model of type theory in cubical sets”, in 19th International Conference on Types for Proofs and Programs (TYPES 2013), Ralph Matthes and Aleksy Schubert (eds), Dagstuhl, Germany: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, pp. 107–128. (Scholar)
Bishop, Errett, 1967, Foundations of constructive analysis, New York-Toronto, Ont.-London: McGraw-Hill Book Co.. (Scholar)
Brady, Edwin C., 2011, “IDRIS: systems programming meets full dependent types”, in Proceedings of the 5th ACM workshop on Programming Languages meets Program Verification (PLPV 2011), pp. 43–54, doi:10.1145/1929529.1929536.
de Bruijn, Nicholas G., 1970, “The mathematical language AUTOMATH, its usage, and some of its extensions”, in Symposium on Automatic Demonstration (Versailles, 1968), Lecture Notes in Mathematics, Vol. 125, Berlin: Springer, pp. 29:61. (Scholar)
Cartmell, John, 1986, “Generalised algebraic theories and contextual categories”, Annals of Pure and Applied Logic, 32: 209–243. (Scholar)
Castellan, Simon, Pierre Clairambault, and Peter Dybjer, 2015: “Undecidability of Equality in the Free Locally Cartesian Closed Category”, TLCA pp 138-152. (Scholar)
Clairambault, Pierre and Peter Dybjer, 2014, “The biequivalence of locally cartesian closed categories and Martin-Löf type theories”, Mathematical Structures in Computer Science, 24(6). doi:10.1017/s0960129513000881 (Scholar)
Coquand, Thierry and Gérard Huet, 1988, “The calculus of constructions”, Information and Computation, 76(2–3): 95–120, doi:10.1016/0890-5401(88)90005-3. (Scholar)
Curien, Pierre-Louis, 1993, “Substitution up to isomorphism”, Fundamentae Informatica, 19: 51–85. (Scholar)
Curry, Haskell B. and Robert Feys, 1958, Combinatory Logic, Amsterdam: North-Holland. (Scholar)
Dybjer, Peter, 1991, “Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics”, in Logical Frameworks, Gérard Huet and Gordon Plotkin (eds), Cambridge: Cambridge University Press, pp. 280–306 . (Scholar)
–––, 1996, “Internal Type Theory”, in Types for Proofs and Programs, TYPES '95, Stefano Berardi and Mario Coppo (eds), Lecture Notes in Computer Science Volume (LNCS), vol. 1158, Heidelberg: Springer-Verlag, pp. 120–134. (Scholar)
–––, 1997, “Representing inductively defined sets by wellorderings in Martin-Löf’s type theory”, Theoretical Computer Science, 176: 329–335. (Scholar)
–––, 2000, “A general formulation of simultaneous inductive-recursive definitions in type theory”, Journal of Symbolic Logic, 65: 525–549.
Dybjer, Peter and Anton Setzer, 1999, “A finite axiomatization of inductive-recursive definitions”, Proceedings of Typed Lambda Calculi and Applications: 4th International Conference (Lecture Notes in Computer Science: 1581), Dordrecht: Springer Verlag.
–––, 2003, “Induction-recursion and initial algebras”, Annals of Pure and Applied Logic, 124: 1–47. (Scholar)
Gonthier, Georges, 2008, “Formal proof of the four-color theorem”, Notices American Mathematical Society, 55: 1382–1393. (Scholar)
Hofmann, Martin, 1994, “Interpretation of Type Theory in Locally Cartesian Closed Categories”, in Proceedings of CSL, Lecture Notes in Computer Science (LNCS), Berlin: Springer-Verlag. doi:10.1007/bfb0022273 (Scholar)
–––, 1995, Extensional concepts in intensional type theory, Ph.D. Thesis, University of Edinburgh. (Scholar)
–––, 1997, “Syntax and semantics of dependent types”, in Semantics and logics of computation, Andrew M. Pitts and P. Dybjer (eds), Publications of the Newton Institure (No.14), Cambridge: Cambridge University Press, pp. 79–130. (Scholar)
Hofmann, Martin and Thomas Streicher, 1998, “The groupoid interpretation of type theory”, in Sambin and Smith 1998: 83–111. (Scholar)
Howard, William A., 1980, “The Formulae-as-Types Notion of Construction”, in To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J.P. Seldin and J.R. Hindley (eds), Academic Press, pp. 479–490. (Scholar)
Jacobs, Bart, 1999, Categorical logic and type theory, Studies in Logic and the Foundations of Mathematics 141, Amsterdam: North-Holland. (Scholar)
Lawvere, F. William, 1970, “Equality in Hyperdoctrines and Comprehension Schema as an Adjoint Functor”, in Proceedings of the American Mathematical Society Symposium on Pure Mathematics XVII, pp. 1–14. (Scholar)
Leroy, Xavier, 2009, “Formal verification of a realistic compiler”, Communications of the ACM, 52(7):107–115. (Scholar)
Lumsdaine, Peter LeFanu, 2010, “Weak omega-categories from intensional type theory”, Logical Methods in Computer Science, 6(3), doi:10.2168/lmcs-6(3:24)2010, [LeFanu Lumsdaine 2010 available online] (Scholar)
Martin-Löf, Per, 1971a, An intuitionistic theory of types, unpublished preprint. (Scholar)
–––, 1971b, “Hauptsatz for the intuitionistic theory of iterated inductive definitions”, in Proceedings of the 2nd Scandinavian logic symposium, J.E. Fenstad (ed.), Amsterdam: North-Holland, pp. 179–216. (Scholar)
–––, 1975, “An intuitionistic theory of types: Predicative part”, in Logic colloquium ’73, H.E. Rose and J. Shepherdson (eds), Amsterdam: North-Holland, pp. 73–118. (Scholar)
–––, 1982, “Constructive mathematics and computer programming”, in Logic, methodology and philosophy of science VI, Proceedings of the 1979 international congress at Hannover, Germany, L.J. Cohen, J. Los, H. Pfeiffer and K.-P. Podewski (eds). Amsterdam: North- Holland Publishing Company, pp. 153–175. (Scholar)
–––, 1984, Intuitionistic type theory: Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980, Napoli: Bibliopolis. (Scholar)
–––, 1986, “Unifying Scott’s theory of domains for denotational semantics and intuitionistic type theory (abstract)”, in Atti del Congresso ’Logica e Filosofia della Scienza, oggi’, San Gimignano, 7–11 December 1983, Vol. I – Logica, CLUEB, Bologna. (Scholar)
–––, 1987, “Truth of a proposition, evidence of a judgment, validity of a proof”, Synthese, 73: 407–420. (Scholar)
–––, 1990, “Mathematics of infinity”, in COLOG-88, P. Martin-Löf and G. Mints (eds), Berlin: Springer, pp. 146–197. (Scholar)
–––, 1994, “Analytic and synthetic judgments in type theory”, in Kant and contemporary epistemology, P. Parrini (ed.), Dordrecht: Kluwer, pp. 87–99. (Scholar)
–––, 1996, “On the meanings of the logical constants and the justifications of the logical laws”, Nordic Journal of Philosophical Logic, 1(1): 11–60. (Scholar)
–––, 1998 [1972], “An intuitionistic theory of types”, in Sambin and Smith 1998: 127–172. (Written in 1972 but unpublished.) (Scholar)
–––, 2009, “100 years of Zermelo’s Axiom of Choice: What was the problem with it?” in Logicism, intuitionism, and formalism: What has become of them?, S. Lindström, E. Palmgren, K. Segerberg, and V. Stoltenberg-Hansen (eds), Dordrecht: Springer, pp. 209–219. (Scholar)
McBride, Conor and James McKinna, 2004, “The view from the left”, Journal of Functional Programming, 14: 69–111. (Scholar)
de Moura, Leonardo, Soonho Kong, Jeremy Avigad, Floris van Doorn and Jakob von Raumer, 2015, “The Lean Theorem Prover”, in 25th International Conference on Automated Deduction (CADE-25), Berlin, Germany. [de Moura et al. 2015 available online] (Scholar)
Nordström, Bengt, Kent Petersson, and Jan M. Smith, 1990, Programming in Martin-Löf’s type theory. An introduction, New York: Oxford University Press. (Scholar)
Norell, Ulf, 2008, “Dependently Typed Programming in Agda”, in Proceedings of the 6th international conference on Advanced Functional Programming, pp. 230–266. (Scholar)
Palmgren, Erik, 1991, On Fixed Point Operators, Inductive Definitions and Universes in Martin-Löf Type Theory, Doctoral dissertation in mathematics, Uppsala University. (Scholar)
–––, 1998, “On universes in type theory”, in Sambin and Smith 1998: 191-204. (Scholar)
–––, 2022, “From type theory to setoids and back”, Mathematical Structures in Computer Science, 32(10): 1283–1312. (Scholar)
Palmgren, Erik and Viggo Stoltenberg-Hansen, 1990 “Domain interpretations of Martin-Löf’s partial type theory”, Annals of Pure and Applied Logic, 48: 135–196. (Scholar)
Paulin-Mohring, Christine, 1993, “Inductive Definitions in the system Coq: Rules and Properties”, in Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA '93, Marc Bezem and Jan F. Groote (eds), Lecture Notes in Computer Science (LNCS), Springer, pp. 328–345. (Scholar)
Pollack, Randy, 1994, The theory of LEGO, PhD Thesis, Edinburgh. (Scholar)
PRL Group, 1986, Implementing Mathematics with the Nuprl Proof Development System, Engelwood Cliffs, NJ: Prentice-Hall. (Scholar)
Ranta, Aarne, 1994, Type-theoretical Grammar, Oxford: Oxford University Press. (Scholar)
Rathjen, Michael, Edward R. Griffor, and Erik Palmgren, 1998, “Inaccessibility in constructive set theory and type theory”, Annals of Pure and Applied Logic, 94: 181–200. (Scholar)
Reynolds, John C., 1984, “Polymorphism is not Set-Theoretic”, in Semantics of Data Types: International Symposium Sophia-Antipolis, France, June 27–29, 1984 Proceedings, Giles Kahn, David B. MacQueen, and Gordon Plotkin (eds), Lecture Notes in Computer Science (LNCS), vol. 173, Springer, pp. 145–156. (Scholar)
Sambin, G. and Jan M. Smith (eds), 1998, Twenty-five years of constructive type theory, Oxford: Clarendon Press. (Scholar)
Scott, Dana S., 1970, “Constructive Validity”, in Symposium on Automatics Demonstration (Versailles, December 1968, M. Laudet, D. Lacombe, L. Nolin, and M. Schützenberg (eds), Lecture Notes in Mathematics, vol. 125, Springer, pp. 237–275. (Scholar)
Seely, Robert A.G., 1984, “Locally cartesian closed categories and type theory”, Mathematical Proceedings of the Cambridge Philosophical Society, 95: 33–48. (Scholar)
Setzer, Anton, 1998, “Well-ordering proofs for Martin-Löf type theory”, Annals of Pure and Applied Logic, 92: 113–159. (Scholar)
–––, 2000, “Extending Martin-Löf type theory by one Mahlo-universe”, Archive for Mathematical Logic, 39: 155–181. (Scholar)
Smith, Jan, 1984, “An interpretation of Martin-Löf’s type theory in a type-free theory of propositions”, Journal of Symbolic Logic, 49: 730–753. (Scholar)
Sundholm, Göran, 2012, “On the Philosophical Work of Per Martin-Löf”, in P. Dybjer, S. Lindström, E. Palmgren, and G. Sundholm (eds), Epistemology versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf, Springer, pp. xxiii–xxiv. (Scholar)
The Univalent Foundations Program, 2013, Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study, Princeton. [The Univalent Foundations Program 2013 available online]. (Scholar)

Generated Tue Oct 1 04:39:53 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 ...