A quem interessar possa Confirmados dias, horários e local:
"*Introdução à Teoria Intuicionística de Tipos*" (Ruy) 4a.feira, 08/02, 15-17hs, Sala D-005 (CIn-UFPE) 5a.feira, 09/02, 13-15hs, Sala D-005 (CIn-UFPE) 6a.feira, 10/02, 13-15hs, Sala D-005 (CIn-UFPE) "*Homotopy Type Theory*" (Peter Lumsdaine) 13 a 17/02, 13-15hs, Sala D-005 (CIn-UFPE) Ruy Em 5 de janeiro de 2012 08:21, Ruy de Queiroz <r...@cin.ufpe.br> 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 <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
