Editing Institute for Advanced Study (section)

==Special Year programs==
Flexner's vision of the kind of results that can emerge in an institution devoted to the pursuit of knowledge for its own sake is illustrated by the "Special Year" programs sponsored by the IAS School of Mathematics.<ref>{{Cite web|url=https://www.math.ias.edu/taxonomy/term/8|archive-url=https://web.archive.org/web/20081222053035/http://www.math.ias.edu/taxonomy/term/8|url-status=dead|archive-date=December 22, 2008|title=Institute for Advanced Study: Special Year Programs}}</ref>   For example, in 2012–13 researchers at the IAS school of mathematics held ''A Special Year on Univalent Foundations of Mathematics''.<ref>{{cite web|url=https://www.math.ias.edu/sp/univalent|title=Univalent Foundations of Mathematics|date=October 21, 2010|access-date=July 19, 2015}}</ref> [[Intuitionistic type theory]] was created by the Swedish logician [[Per Martin-Löf]] in 1972 to serve as an alternative to set theory as a foundation for mathematics.  The special year brought together researchers in [[topology]], [[computer science]], [[category theory]], and [[mathematical logic]] with the goal of formalizing and extending this theory of foundations.  The program was organized by [[Steve Awodey]], [[Thierry Coquand]] and [[Vladimir Voevodsky]], and resulted in a book being published in [[homotopy type theory]].<ref name=hott>{{Cite web|url=http://hottheory.files.wordpress.com/2013/03/hott-online-611-ga1a258c.pdf|title=Homotopy Type Theory: Univalent Foundations of Mathematics}}</ref>  The authors—more than 30 researchers ultimately contributed to the project—noted the essential contribution of the IAS saying,

{{quote|text=Special thanks are due to the Institute for Advanced Study, without which this book would obviously never have come to be. It proved to be an ideal setting for the creation of this new branch of mathematics: stimulating, congenial, and supportive. May some trace of this unique atmosphere linger in the pages of this book, and in the future development of this new field of study.|title=The Univalent Foundations Program|source=Institute for Advanced Study Princeton, April 2013<ref name=hott/>}}

One of the researchers, Andrej Bauer said,

{{quote|text=We are a group of two dozen mathematicians who wrote a 600 page book in less than half a year. This is quite amazing, since mathematicians do not normally work together in large groups.  But more importantly, the spirit of collaboration that pervaded our group at the Institute for Advanced Study was truly amazing. We did not fragment. We talked, shared ideas, explained things to each other, and completely forgot who did what.|author=Andrej Bauer|source=Mathematics and Computation, June 20, 2013<ref>{{cite web|url=http://math.andrej.com/2013/06/20/the-hott-book/|title=The HoTT book (finished)|access-date=19 July 2015}}</ref>}}

The book, informally known as ''The HoTT book'', is freely available online.<ref>{{cite web|title=The HoTT Book (obtaining)|url=https://homotopytypetheory.org/book/|website=Homotopy Type Theory|date=March 12, 2013|access-date=December 10, 2017|archive-url=https://web.archive.org/web/20180813123314/https://homotopytypetheory.org/book/|archive-date=August 13, 2018|url-status=dead}}</ref>