Car*s, A vinda de Voevodsky para dar um curso de Verão no Departamento de Matemática da UFPE está bem encaminada. Muito provavelmente, o curso deverá ocorrer na segunda metade de Fevereiro de 2012.
Aproveito para informar que, motivado pela palestra de Voevodsky no WoLLIC 2011, decidí expandir o artigo publiquei no número especial da ENTCS com as contribuições do LSFA 2010, resultando num material que depositei no arxiv.org: Propositional equality, identity types, and direct computational paths http://arxiv.org/abs/1107.1901 O artigo foi submetido à publicação. Comentários são muito bem-vindos. Abraço, Ruy Em 14 de junho de 2011 15:48, Ruy de Queiroz <r...@cin.ufpe.br> escreveu: > João Marcos, > > Em 14 de junho de 2011 11:58, Joao Marcos <botoc...@gmail.com> escreveu: > > Talvez alguém que tenha comparecido ao WoLLIC deste ano possa nos >> explicar um pouco mais sobre os tais "Univalent Foundations of >> Mathematics"? >> >> http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2011_WoLLIC.pdf >> >> Estive lá, sim. Mas não há como ser mais preciso por e-mail do que o > material que ele próprio disponibiliza. > > Como já foi dito por Valéria, o foco não é no problema da possível > (in)consistência da aritmética, mas na busca por novos fundamentos da > matemática com base na teoria de tipos de Martin-Löf (alternativamente a > ZFC). Como especialista em teoria da homotopia, Voevodsky está procurando > encontrar paralelos entre as construções da teoria construtiva de tipos (em > particular, o cálculo de construções) e os tipos de homotopia. E até mesmo > implementar as construções no sistema Coq. Segundo ele mesmo diz na sua > motivação, o ponto de partida foi o modelo grupóide da teoria de tipos > intensional construído por Martin Hofmann e Thomas Streicher ("The Groupoid > Model Refutes Uniqueness of Identity Proofs", LICS 1994). > > Aqui na UFPE estamos (eu e Luciana Vale, aluna do doutorado da Matemática) > tentando fazer uma leitura desse modelo a partir da reformulação da > interpretação funcional da igualdade proposicional que começamos a elaborar > desde o 9th Amsterdam Coll (1994), e que mais recentemente foi apresentada > no LSFA 2010 ("The Functional Interpretation of Direct Computations"). > > Propus à Matemática trazer Voevodsky para o próximo Programa de Verão. Caso > se confirme, divulgo na lista. > > Abraço, > > Ruy > > > JM >> >> 2011/6/6 Valeria de Paiva <valeria.depa...@gmail.com>: >> > Marcelo, >> > >> > eu nem assisti a palestra ainda, mas todas as discusses que li, dizem >> que o >> > apelo 'e pra uma fundamentacao usando Martin-Loeuf's teoria de tipos. >> > >> > abs >> > Valeria >> > >> > 2011/6/6 Marcelo Finger <mfin...@ime.usp.br> >> >> >> >> Acho que é um apelo por uma fundamentação paraconsistente. >> >> >> >> >> >> 2011/6/6 Joao Marcos <botoc...@gmail.com> >> >> >> >> > "What if current foundations of mathematics are inconsistent?" >> >> > - Institute for Advanced Study, Princeton >> >> > http://video.ias.edu/voevodsky-80th >> >> > >> >> > >> >> > Have fun, >> >> > JM >> >> > _______________________________________________ >> >> > Logica-l mailing list >> >> > Logica-l@dimap.ufrn.br >> >> > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l >> >> > >> >> >> >> >> >> >> >> -- >> >> Marcelo Finger >> >> Departamento de Ciencia da Computacao >> >> Instituto de Matematica e Estatistica >> >> Universidade de Sao Paulo >> >> Rua do Matao, 1010 >> >> 05508-090 Sao Paulo, SP Brazil >> >> Tel: +55 11 3091-9688, 3091-6135, 3091-6134 (fax) >> >> http://www.ime.usp.br/~mfinger >> >> _______________________________________________ >> >> Logica-l mailing list >> >> Logica-l@dimap.ufrn.br >> >> 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/ >> > >> >> >> >> -- >> http://sequiturquodlibet.googlepages.com/ >> _______________________________________________ >> Logica-l mailing list >> Logica-l@dimap.ufrn.br >> http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l >> > > _______________________________________________ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
