Confirmados dias, horários e salas do mini-curso de Michael Warren (Princeton) no Programa de Verão da DMAT-UFPE 2013<http://www.dmat.ufpe.br/~verao2013/> :
28/01 14h-18h Anfiteatro do Centro de Informática 29/01 15h-18h Anfiteatro do Centro de Informática 30/01 14h-18h Anfiteatro do Centro de Informática 31/01 14h-18h Auditório (1o. andar) do Centro de Informática 01/02 14h-18h Anfiteatro do Centro de Informática Aproveito para indicar a leitura de um artigo de Michael Warren, justamente sobre o tópico do mini-curso de verão. Ruy P.S. Para quaisquer informações sobre o Programa de Verão DMAT 2013, visite http://www.dmat.ufpe.br/~verao2013/ ---- Homotopy type theory and Voevodsky's univalent foundations<http://arxiv.org/abs/1210.5658> Álvaro Pelayo <http://arxiv.org/find/math/1/au:+Pelayo_A/0/1/0/all/0/1>, Michael A. Warren <http://arxiv.org/find/math/1/au:+Warren_M/0/1/0/all/0/1> (Submitted on 20 Oct 2012) 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. Comments:48 pages, 14 figuresSubjects:Logic (math.LO); Logic in Computer Science (cs.LO); Algebraic Topology (math.AT)Cite as:arXiv:1210.5658<http://arxiv.org/abs/1210.5658> [math.LO] (or arXiv:1210.5658v1 <http://arxiv.org/abs/1210.5658v1> [math.LO] for this version) 2012/12/3 Ruy de Queiroz <r...@cin.ufpe.br> > Caros, > > Estamos trazendo Michael Warren <http://www.math.ias.edu/~mwarren/>, do > Institute of Advanced Study, Princeton, (da equipe de Vladimir Voevodsky), > para ministrar um mini-curso de "Homotopy Type Theory" no Programa de Verão > da Matemática da UFPE de 2013, a ser realizado no periodo de 28/01 a 02/02. > > Esperamos contar com a presença de todos os interessados no tema. > > Abraço, > Ruy > ------ > > > TITLE: > > Types and homotopy types > > ABSTRACT: > > In this series of lectures I will give an introduction to recent research > in what has been called "homotopy type theory" and to Voevodsky's > "univalent foundations" program. Both of these areas of research involve > connections between homotopy theory, higher-dimensional category theory and > type theory, and we aim to introduce sufficient background in all of these > areas for attendees to appreciate these connections. Particular attention > will be paid to issues related to proving results in homotopy theory in > this setting including the question of how to represent spaces as datatypes. > > BIO: > > Dr. Warren completed his Ph.D. thesis, entitled "Homotopy Theoretic > Aspects of Constructive Type Theory" and supervised by Prof. Steven Awodey, > at Carnegie Mellon University in 2008. He was then a Fields Institute > Postdoctoral Fellow at the University of Ottawa, where he was a member of > the Logic and Foundations of Computing Group, from 2008 to 2010. During the > 2010 academic year he was an AARMS Postdoctoral Fellow working in > the Atlantic Category Theory Group at Dalhousie University. Since 2011 he > has been a Member of the School of Mathematics at the Institute for > Advanced Study. His research is in the areas of category theory, > mathematical logic, algebraic topology, and theoretical computer science. > ------------------------- > > > > > > _______________________________________________ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
