| Publication | Date of Publication | Type |
|---|
Kripke-Joyal forcing for type theory and uniform fibrations
Selecta Mathematica. New Series | 2024-08-13 | Paper |
Cartesian cubical model categories
| 2023-05-01 | Paper |
scientific article; zbMATH DE number 7599486 (Why is no real title available?)
| 2022-10-11 | Paper |
On Hofmann-Streicher universes
| 2022-05-22 | Paper |
Sheaf Representations and Duality in Logic
Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics | 2021-12-08 | Paper |
Kripke-Joyal forcing for type theory and uniform fibrations
| 2021-10-27 | Paper |
Impredicative encodings of (higher) inductive types
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-20 | Paper |
Mathesis Universalis and Homotopy Type Theory
Mathesis Universalis, Computability and Proof | 2020-08-10 | Paper |
A proposition is the (homotopy) type of its proofs
| 2019-10-15 | Paper |
A cubical model of homotopy type theory
Annals of Pure and Applied Logic | 2018-10-18 | Paper |
Univalence as a principle of logic
Indagationes Mathematicae. New Series | 2018-10-08 | Paper |
Homotopy-initial algebras in type theory
Journal of the ACM | 2018-08-02 | Paper |
Carnap and the invariance of logical truth
Synthese | 2018-03-27 | Paper |
Polynomial pseudomonads and dependent type theory
| 2018-02-03 | Paper |
Natural models of homotopy type theory
Mathematical Structures in Computer Science | 2018-01-11 | Paper |
Inductive types in homotopy type theory
2012 27th Annual IEEE Symposium on Logic in Computer Science | 2017-05-16 | Paper |
Topos Semantics for Higher-Order Modal Logic
| 2017-04-11 | Paper |
A cubical model of homotopy type theory
| 2016-07-21 | Paper |
Voevodsky’s Univalence Axiom in Homotopy Type Theory
Notices of the American Mathematical Society | 2015-10-14 | Paper |
From sets to types, to categories, to sets
The Western Ontario Series in Philosophy of Science | 2015-07-01 | Paper |
Type theory and homotopy
Epistemology versus Ontology | 2015-06-05 | Paper |
Structuralism, Invariance, and Univalence
Philosophia Mathematica | 2015-04-17 | Paper |
Homotopy Type Theory
Logic and Its Applications | 2015-01-09 | Paper |
scientific article; zbMATH DE number 6302891 (Why is no real title available?)
| 2014-06-11 | Paper |
Martin-Löf complexes
Annals of Pure and Applied Logic | 2013-12-11 | Paper |
Relating first-order set theories, toposes and categories of classes
Annals of Pure and Applied Logic | 2013-12-10 | Paper |
First-order logical duality
Annals of Pure and Applied Logic | 2013-02-19 | Paper |
Kripke Semantics for Martin-L\"of's Extensional Type Theory
Logical Methods in Computer Science | 2012-04-02 | Paper |
scientific article; zbMATH DE number 5859784 (Why is no real title available?)
| 2011-03-02 | Paper |
TOPOLOGY AND MODALITY: THE TOPOLOGICAL INTERPRETATION OF FIRST-ORDER MODAL LOGIC
The Review of Symbolic Logic | 2010-08-13 | Paper |
scientific article; zbMATH DE number 5761737 (Why is no real title available?)
| 2010-07-27 | Paper |
Lawvere–Tierney sheaves in Algebraic Set Theory
Journal of Symbolic Logic | 2009-09-29 | Paper |
Kripke Semantics for Martin-Löf’s Extensional Type Theory
Lecture Notes in Computer Science | 2009-07-07 | Paper |
A Brief Introduction to Algebraic Set Theory
The Bulletin of Symbolic Logic | 2009-03-25 | Paper |
Homotopy theoretic models of identity types
Mathematical Proceedings of the Cambridge Philosophical Society | 2009-01-30 | Paper |
Relating First-Order Set Theories and Elementary Toposes
The Bulletin of Symbolic Logic | 2008-10-23 | Paper |
Sheaf toposes for realizability
Archive for Mathematical Logic | 2008-08-18 | Paper |
Carnap's dream: Gödel, Wittgenstein, and \textit{Logical Syntax}
Synthese | 2007-11-14 | Paper |
scientific article; zbMATH DE number 5180960 (Why is no real title available?)
| 2007-08-20 | Paper |
In Memoriam: Saunders Mac Lane 1909–2005
The Bulletin of Symbolic Logic | 2007-08-08 | Paper |
Category Theory
| 2006-06-13 | Paper |
scientific article; zbMATH DE number 2222244 (Why is no real title available?)
| 2005-11-02 | Paper |
Ultrasheaves and double negation
Notre Dame Journal of Formal Logic | 2005-07-06 | Paper |
scientific article; zbMATH DE number 2172973 (Why is no real title available?)
| 2005-06-01 | Paper |
Propositions as [Types]
Journal Of Logic And Computation | 2004-10-28 | Paper |
An Answer to Hellman's Question: ‘Does Category Theory Provide a Framework for Mathematical Structuralism?’†
Philosophia Mathematica | 2004-06-22 | Paper |
Completeness and Categoricity, Part II: Twentieth-Century Metalogic to Twenty-first-Century Semantics
History and Philosophy of Logic | 2003-10-28 | Paper |
Completeness and Categoricity. Part I: Nineteenth-century Axiomatics to Twentieth-century Metalogic
History and Philosophy of Logic | 2003-10-13 | Paper |
Elementary axioms for local maps of toposes
Journal of Pure and Applied Algebra | 2003-03-09 | Paper |
Modal operators and the formal dual of Birkhoffs completeness theorem This research is part of the Logic of Types and Computation project at Carnegie Mellon University under the direction of Dana Scott.
Mathematical Structures in Computer Science | 2003-01-01 | Paper |
Local realizability toposes and a modal logic for computability
Mathematical Structures in Computer Science | 2002-10-31 | Paper |
Carnap, completeness, and categoricity: The Gabelbarkeitssatz of 1928
Erkenntnis | 2002-07-05 | Paper |
Topological completeness for higher-order logic
Journal of Symbolic Logic | 2002-01-21 | Paper |
scientific article; zbMATH DE number 1497740 (Why is no real title available?)
| 2001-03-06 | Paper |
Sheaf representation for topoi
Journal of Pure and Applied Algebra | 2000-09-17 | Paper |
Topological representation of the λ-calculus
Mathematical Structures in Computer Science | 2000-04-13 | Paper |
Structure in Mathematics and Logic: A Categorical Perspective
Philosophia Mathematica | 1997-10-14 | Paper |
