Excelente Ruy! obrigada, Valeria 2012/2/25 Ruy de Queiroz <[email protected]>
> Aos interessados: uma parte do material do curso de Lumsdaine foi por ele > disponibilizado em: > > http://www.mathstat.dal.ca/~p.l.lumsdaine/misc_files/2012-02-recife/ > > Ruy > > > Em 5 de janeiro de 2012 08:21, Ruy de Queiroz <[email protected]> escreveu: > > > 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 <[email protected]> > > 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 <[email protected]>, posgrad <[email protected]>, grad-l < > > [email protected]> > > > > > > > > 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 [email protected] > > > > 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 > [email protected] > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l > -- Valeria de Paiva http://www.cs.bham.ac.uk/~vdp/ http://valeriadepaiva.org/www/ _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
