Na próxima terça-feira, 18, às 11h, na sala 2077 do Instituto de Ciências Exatas (ICEx) da UFMG, o apresentador do podcast Type Theory Forall (https://typetheoryforall.com), Pedro Abreu, irá proferir a palestra “Se Alan Turing é o Pai da Computação, Alonzo Church é a Mãe — O Rico Contexto Histórico Por Trás da Ciência da Computação”.
Pedro Abreu é graduado em Ciência da Computação pela Universidade de Brasília. mestre pela Purdue Universidade (Indiana – USA), além de apresentador do podcast Type Theory Forall, Pedro também fez vários estágios e consultorias nas áreas de teste e verificação formal de programas, entre eles: Tribunal de Contas da União (Brasília), SiFive (San Mateo, Vale do Silício), Galois (Porland, Oregon), Nomadic Labs (Paris),
Sobre a palestra:
Todos sabemos que Alan Turing é considerado o pai da computação por ter inventado a “Máquina de Turing” no auge de seus 24 anos de idade. Mas nem todos conhecem como a história da computação está intimamente ligada não apenas a computadores, mas também à lógica e aos próprios limites formais da matemática.
Nesta palestra, vou contar um pouco sobre o rico contexto histórico por trás da invenção da Máquina Universal de Turing, os Problemas de Hilbert, os Teoremas da Incompletude de Gödel, os Teoremas de Indefinibilidade de Tarski, o Cálculo Lambda de Alonzo Church e sua equivalência com as máquinas de Turing. Finalmente, falarei um pouco sobre o conceito de equivalência entre programas e provas descrito pelo belíssimo Teorema do Isomorfismo de Curry-Howard e como, a partir daí, nasce todo o conceito de provas formais assistidas por computadores, estudadas pela Teoria dos Tipos Dependentes.
