American Mathematical Society

My Account · My Cart · Customer Services · FAQ  
joint mathematics meetings
notices november 2014
math moments 111
ams election 2014
about the ams
Serving the Community
Mathematics Awareness
In the News
Events & Announcements
Publishing Highlights

AMS Response to Swets Bankruptcy Filing

The AMS will work individually with all institutions that paid for 2015 subscriptions to AMS products through Swets & Zeitlinger Group BV, prior to their announcement on September 22, 2014, to ensure that institutions receive uninterrupted access to our publications and database products. Read the full response from Associate Executive Director, Publishing Robert Harington.

Featured Publication

Turbulent Times in Mathematics: The Life of J.C. Fields and the History of the Fields Medal
Elaine McKinnon Riehm and Frances Hoffman

"This highly readable nonmathematical biographical study is a triumph of tenacity. It sheds significant light on the personal life, professional development, and lasting legacy of the foremost Canadian mathematician of his time."

--Deborah Kent, Isis, Vol. 105, No. 2 (June 2014)

Turbulent Times in Mathematics: The Life of J.C. Fields and the History of the Fields Medal
Elaine McKinnon Riehm and Frances Hoffman

"This highly readable nonmathematical biographical study is a triumph of tenacity. It sheds significant light on the personal life, professional development, and lasting legacy of the foremost Canadian mathematician of his time."

--Deborah Kent, Isis, Vol. 105, No. 2 (June 2014)

Bulletin of the AMS

Bulletin of the AMS Homotopy type theory and Voevodsky's univalent foundations
( view abstract )
Homotopy type theory and Voevodsky's univalent foundations
Recent discoveries have been made connecting abstract homotopy theory and the field of type theory from logic and theoretical computer science. This has given rise to a new field, which has been christened homotopy type theory. In this direction, Vladimir Voevodsky observed that it is possible to model type theory using simplicial sets and that this model satisfies an additional property, called the Univalence Axiom, which has a number of striking consequences. He has subsequently advocated a program, which he calls univalent foundations, of developing mathematics in the setting of type theory with the Univalence Axiom and possibly other additional axioms motivated by the simplicial set model. Because type theory possesses good computational properties, this program can be carried out in a computer proof assistant. In this paper we give an introduction to homotopy type theory in Voevodsky's setting, paying attention to both theoretical and practical issues. In particular, the paper serves as an introduction to both the general ideas of homotopy type theory as well as to some of the concrete details of Voevodsky's work using the well-known proof assistant Coq. The paper is written for a general audience of mathematicians with basic knowledge of algebraic topology; the paper does not assume any preliminary knowledge of type theory, logic, or computer science. Because a defining characteristic of Voevodsky's program is that the Coq code has fundamental mathematical content, and many of the mathematical concepts which are efficiently captured in the code cannot be explained in standard mathematical English without a lengthy detour through type theory, the later sections of this paper (beginning with Section [*]) make use of code; however, all notions are introduced from the beginning and in a self-contained fashion.


Browse the archive 1891 - 2014.

Research Journals Spotlight
 
JAMS
loading...
MCOM
loading...
PROC
loading...
BTran
loading...
TRAN
loading...
BProc
loading...
ECGD
loading...
ERT
loading...