A
BibTeX entry for this reference:
@Article{awodey_2018_natural-models-of-homotopy-type-theory,
author = {Awodey, Steve},
title = {Natural models of homotopy type theory},
journal = {Math. Structures Comput. Sci.},
year = 2018,
volume = 28,
number = 2,
pages = {241-286},
fjournal = {Mathematical Structures in Computer Science. A Journal in the Applications of Categorical, Algebraic and Geometric Methods in Computer Science},
issn = {0960-1295},
mrclass = {03B15 (03G30 18G55 55U35)},
mrnumber = 3742564,
mrreviewer = {Fredrik Nordvall Forsberg},
doi = {10.1017/S0960129516000268},
url = {https://doi.org/10.1017/S0960129516000268},
eprint = {1406.3219}
}K
BibTeX entry for this reference:
@Misc{kapulkin_2012_the-simplicial-model-of-univalent-foundations,
author = {Kapulkin, Krzysztof and Lumsdaine, Peter LeFanu},
title = {The simplicial model of univalent foundations (after Voevodsky)},
year = 2012,
note = {Revised 2018 as v5},
eprint = {1211.2851}
}S
BibTeX entry for this reference:
@Book{streicher_1991_semantics-of-type-theory,
author = {Streicher, Thomas},
title = {Semantics of type theory},
publisher = {Birkh\"{a}user Boston, Inc., Boston, MA},
year = 1991,
series = {Progress in Theoretical Computer Science},
note = {Correctness, completeness and independence results, With a foreword by Martin Wirsing},
pages = {xii+298},
isbn = {0-8176-3594-7},
mrclass = {68Q55 (03B40 03B70 03F50 06B35 68Q65)},
mrnumber = 1134134,
mrreviewer = {John C. Mitchell},
doi = {10.1007/978-1-4612-0433-6},
url = {https://doi.org/10.1007/978-1-4612-0433-6}
}V
BibTeX entry for this reference:
@Misc{voevodsky_2015_hott-is-not_an-interpretation-of-mltt-into-abstract-homotopy-theory,
author = {Voevodsky, Vladimir},
title = {HoTT is not an interpretation of MLTT into abstract homotopy theory},
year = 2015,
note = {Article at the {\url{homotopytypetheory.org}} blog, January 11, 2015},
url = {https://homotopytypetheory.org/2015/01/11/hott-is-not-an-interpretation-of-mltt-into-abstract-homotopy-theory/}
}BibTeX entry for this reference:
@Misc{voevodsky_2015_from-syntax-to-semantics-of-dependent-type-theories,
author = {Voevodsky, Vladimir},
title = {From syntax to semantics of dependent type theories --- formalized},
howpublished = {Slides},
year = 2015,
note = {Lecture at RDP 2015, Warsaw, June 30, 2015},
url = {https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2015_06_30_RDP.pdf}
}
BibTeX entry for this reference:
@Misc{voevodsky_2016_mathematical-theory-of-type-theories,
author = {Voevodsky, Vladimir},
title = {Mathematical theory of type theories and the initiality conjecture},
year = 2016,
note = {Research proposal to the Templeton Foundation},
url = {https://www.math.ias.edu/Voevodsky/voevodsky-publications_abstracts.html#TempletonProposal}
}BibTeX entry for this reference:
@Misc{voevodsky_2017_the-meta-theory-of-dependent-type-theories,
author = {Voevodsky, Vladimir},
title = {The meta-theory of dependent type theories},
howpublished = {Video},
year = 2017,
note = {Members Seminar, Institute for Advanced Study, Princeton, NJ, USA, February 27, 2017},
url = {https://video.ias.edu/membsem/2017/0227-VladimirVoevodsky}
}BibTeX entry for this reference:
@Misc{voevodsky_2017_models-interpretations-and-the-initiality-conjectures,
author = {Voevodsky, Vladimir},
title = {Models, interpretations and the initiality conjectures},
year = 2017,
note = {Lecture at the special session on category theory and type theory in honor of Per Martin-L{\"o}f on his 75th birthday, August 17--19, 2017, during the Logic Colloquium 2017, August 14--20, 2017, Stockholm},
url = {https://www.math.ias.edu/Voevodsky/voevodsky-publications_abstracts.html#logcoll-1}
}Last revised on October 31, 2018 at 14:04:00. See the history of this page for a list of all contributions to it.