Carnegie Mellon University

Steve Awodey

Professor of Philosophy

135F Baker Hall
Department of Philosophy, courtesy appointment in Mathematical Sciences
Dietrich College of Humanities and Social Sciences
Carnegie Mellon University
5000 Forbes Avenue
Pittsburgh, PA 15213

P: 412-268-8947



Person's Name


Ph.D., University of Chicago


Homotopy Type Theory and Univalent Foundations. More information on this research program can be found on the site Information on the special year 2012-13 on Univalent Foundations at the Institute for Advanced Study can be found on the UF-wiki.

Algebraic Set Theory. A website containing some information about AST and links to some papers.

Select Publications

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

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

A brief introduction to algebraic set theory.    S. Awodey, The Bulletin of Symbolic Logic, 2008.

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

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

Sheaf toposes for realizability (2004).  S. Awodey and A. Bauer, Archive for Mathemtical Logic, 2008.

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).

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

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

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

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.

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.

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.

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

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

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

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.

Axiom of choice and excluded middle in categorical logic. Unpublished MS (1995).