A quem interessar possa As datas do curso de Peter Lumsdaine estão confirmadas para:
13 a 17 de Fevereiro 23 e 24 de Fevereiro Estarei dando umas aulas de introdução ao assunto na semana anterior: 8 a 10 de Fevereiro As aulas deverão ocorrer no Departamento de Matemática da UFPE, e a sala ainda está para ser confirmada. Ruy ---------- Mensagem encaminhada ---------- De: Ruy de Queiroz <r...@cin.ufpe.br> Data: 24 de novembro de 2011 22:58 Assunto: Curso de Verão (Depto de Matemática): "Homotopy Type Theory", por Peter Lumsdaine Para: staff <st...@cin.ufpe.br>, posgrad <posg...@cin.ufpe.br>, grad-l < gra...@cin.ufpe.br> Como parte do Programa de Verão 2012<http://www.ufpe.br/verao/index.php?option=com_content&view=article&id=315&Itemid=243> (Departamento de Matemática – UFPE, 05 de Janeiro a 24 de Fevereiro de 2012), está confirmado o mini-curso sobre teoria dos tipos da homotopia, que pode interessar tanto a matemáticos quanto a cientistas da computação que trabalham com teoria dos tipos, semântica de linguagens de programação, provadores automáticos de teorema, e/ou teoria das categorias. Detalhes sobre inscrição podem ser obtidos por meio de solicitação por e-mail a verao2012.d...@ufpe.br Ruy --- Title: *Homotopy Type Theory* Instructor: Peter Lumsdaine <http://mathstat.dal.ca/~p.l.lumsdaine/>(Dalhousie University, Canada) 15 Feb 2012 - 24 Feb 2012 Abstract: These talks will provide an introduction to Homotopy Type Theory -- the exploration of a fascinating and fruitful connection between logic and algebraic topology that has emerged over the last few years. Dependent Type Theory is a logical system expressive enough to give a foundation for mathematics, but at the same time very well-suited to computer implementation. In particular, if provides the basic language of many proof assistants and formalisation systems -- in particular, Coq. For the most part, its connection to more traditional set-theoretic foundations is clear and well-understood, and moving between the two does not require too much change in technique. An exception to this is its treatment of equality, which seems considerably more subtle than in classical foundations (for reasons originally motivated by philosophical and computational considerations). The key idea of Homotopy Type Theory is that this strangeness is resolved if one considers types as corresponding not to classical sets, but to classical *spaces* (among which sets can still be discerned as the discrete spaces). The subtlety of equality can then be understood as coming from the behavious of *paths* within a space, and be tamed using the insights of modern algebraic topology. Practically, this opens up applications in both directions: tools and intuitions for working in the type theory on the one hand; and on the other hand, a very direct approach to the formalisation of algebraic topology. More philosophically, it gives a new and beautiful outlook on the universe of mathematics, with spaces investigated not indirectly as constructed models, but as fundamental objects of the language, as basic as sets are in the classical picture. Besides introducing the general setting, I will discuss Voevodsky's Univalence Axiom (a strengthening of standard universe axioms), the concept of h-level (homotopical dimension), and higher inductive types (a technique for presenting a wide class of spaces, including cell complexes, within the type theory). I'll use the Coq proof assistant for some exercises and examples. I won't assume previous familiarity with it, but I recommend getting it and trying out the interface beforehand. It's available from http://coq.inria.fr/, and there are several good introductions online; I recommend the first few exercises from http://www.cis.upenn.edu/~bcpierce/sf/toc.html. Warning: Coq can be dangerously addictive! (In the words of Andrew Appel: Coq is the world's best video game.) Much more reading (both light and heavy) on Homotopy Type Theory can be found at http://homotopytypetheory.org. _______________________________________________ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
