Steve Awodey's GitHub pages

View My GitHub Profile

Steve Awodey

Professor, Philosophy and Mathematics

Carnegie Mellon University








  • Polynomial pseudomonads and dependent type theory. S. Awodey, C. Newstead, February 2018. arXiv:1802.00997

  • A proposition is the (homotopy) type of its proofs. January 2016. arXiv:1701.02024

  • Homotopy and type theory (Project description). October 2009. Unpublished grant proposal

  • Axiom of choice and excluded middle in categorical logic. Spring 1995. Unpublished MS


  • Impredicative encodings of (higher) inductive types. S. Awodey, J. Frey, S. Speight, Logic in Computer Science (LICS 2018). arXiv:1802.02820

  • Univalence as a principle of logic. Indagationes Mathematicae: Special Issue L.E.J. Brouwer, 50 years later, D. van Dalen, et al. (ed.s), 2018. preprint

  • A cubical model of homotopy type theory. Annals of Pure and Applied Logic, 2018. arXiv:1607.06413

  • Homotopy-initial algebras in type theory. S. Awodey, N. Gambino, K. Sojakova, Journal of the Association for Computing Machinery, 2017. arXiv:1504.05531

  • Natural models of homotopy type theory. Mathematical Structures in Computer Science, December 2016. arXiv:1406.3219

  • Topos semantics for higher-order modal logic. S. Awodey, K. Kishida, H.-C. Kotzsch, Logique & Analyse, February 2014. arXiv:1403.0020

  • Univalent foundations and the large scale formalization of mathematics. S. Awodey, T. Coquand, The IAS Letter, Institute for Advanced Study, Spring 2013. pdf

  • Structuralism, invariance, and univalence. Philosophia Mathematica, 2013. pdf

  • Voevodsky's univalence axiom in homotopy type theory. S. Awodey, A. Pelayo, and M. Warren, Notices of the American Mathematical Sciety, 2013. pdf

  • Type theory and homotopy. In Dybjer, P., Lindström, Sten, Palmgren, Erik (eds.), Epistemology versus Ontology: Essays on the Foundations of Mathematics in Honour of Per Martin-Löf. Springer, 2010. arXiv:1010.1810

  • First-order logical duality. S. Awodey and H. Forssell, Annals of Pure and Applied Logic, 2013. arXiv:1008.3145

  • Martin-Löf complexes. S. Awodey, P. Hofstra, M. Warren, 2009. pdf

  • From sets, to types, to categories, to sets. 2009. pdf

  • Algebraic models of theories of sets and classes in categories of ideals. S. Awodey, H. Forssell, M. Warren, June 2006.

  • Relating topos theory and set theory via categories of classes. S. Awodey, C. Butz, A. Simpson, T. Streicher. Bulletin of Symbolic Logic, June 2003. Research announcement

  • Lawvere-Tierney sheaves in algebraic set theory. S. Awodey, N. Gambino, P. Lumsdaine, M. Warren. Journal of Symbolic Logic, 2009. pdf

  • Homotopy theoretic models of identity types. S. Awodey, M. Warren. Mathematical Proceedings of the Cambridge Philosophical Society, 2009. pdf

  • Relating first-order set theories, toposes and categories of classes. Steve Awodey, Carsten Butz, Alex Simpson, and Thomas Streicher. Annals of Pure and Applied Logic, 2013. pdf

  • A brief introduction to algebraic set theory. The Bulletin of Symbolic Logic, 2008. pdf

  • Topology and modality: The topological interpretation of first-order modal logic. S. Awodey, K. Kishida, The Review of Symbolic Logic, 2008. pdf

  • Saunders Mac Lane (memorial notice). Proceedings of the American Philosophical Society, 2007. pdf

  • Carnap's Dream: Gödel, Wittgenstein, and Logical Syntax. S. Awodey, A.W. Carus, Synthese, 2007. pdf

  • Sheaf toposes for realizability. S. Awodey and A. Bauer, Archive for Mathemtical Logic, 2008. pdf

  • Algebraic models of intuitionistic theories of sets and classes. S. Awodey and H. Forssell, Theory and Applications of Categories, 15(5), CT 2004, pp. 147--163 (2004). pdf

  • Predicative algebraic set theory. S. Awodey and M. Warren, Theory and Applications of Categories, 15(1), CT 2004, pp. 1--39 (2004). pdf

  • Ultrasheaves and double negation. S. Awodey and J. Eliasson, Notre Dame Journal of Formal Logic, 45(4), pp. 235--245 (2004). pdf

  • Propositions as [types]. S. Awodey and A. Bauer, Journal of Logic and Computation, 14(4), pp. 447--471 (2004). pdf

  • An answer to G. Hellman's question `Does category theory provide a framework for mathematical structuralism?' Philosophia Mathematica, (3), vol. 12 (2004), pp. 54--64. pdf

  • Modal operators and the formal dual of Birkhoff's completeness theorem. S. Awodey and J. Hughes, Mathematical Structures in Computer Science, vol. 13 (2003), pp. 233-258.

  • Categoricity and completeness: 19th century axiomatics to 21st century semantics. S. Awodey and E. Reck, History and Philosophy of Logic, 23 (2002), pp. 1-30, 77-94.

  • Elementary axioms for local maps of toposes. S. Awodey and L. Birkedal, Journal of Pure and Applied Algebra, 177 (2003), pp. 215-230. pdf

  • Local realizability toposes and a modal logic for computability. S. Awodey, L. Birkedal, D.S. Scott, Mathematical Structures in Computer Science, vol. 12 (2002), pp. 319-334. pdf

  • Topological completeness for higher-order logic. S. Awodey and C. Butz, Journal of Symbolic Logic, 65(3), (2000) pp. 1168--82. pdf

  • Topological representation of the lambda-calculus. Mathematical Structures in Computer Science, vol. 10, (2000) pp. 81--96, pdf

  • Sheaf representation for topoi. Journal of Pure and Applied Algebra, 145 (2000), pp. 107--121. pdf

  • Carnap, completeness, and categoricity: The Gabelbarkeitssatz of 1928. S. Awodey and A.W. Carus, Erkenntnis 54 (2001), pp. 145-172.

  • Structure in mathematics and logic: a categorical perspective. Philosophia Mathematica (3), vol. 4 (1996), pp. 209--237.





Steve Awodey, Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA 15213 USA

Office BH 135F, Phone (412) 268-8947, Email awodey(at)cmu(dot)edu