Obrigado Fernando Yamauti. A pergunta sobre "teoria dos tipos" é genérica, mas sua resposta é ampla. W.
Em 20 de dezembro de 2017 00:10, Fernando Yamauti <fgyama...@gmail.com> escreveu: > As referências em https://ncatlab.org/nlab/show/pure+type+system caso busque > o mais geral possível. Para algo mais básico, acho melhor começar com > untyped lambda cálculo, algo como em > http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf > ou no livro do Barendregt, e entender as relações com máquinas de Turing e > funções parcias recursivas. Depois da para ir para simple typed e ir > aumentando a ordem e dependência até pure type systems. > > Para a relação com lógica categorial, eu gosto do livro do Bart Jacobs > https://books.google.com.br/books/about/Categorical_Logic_and_Type_Theory.html?id=0hhyL4WG3ngC&redir_esc=y > . > > Falar "teoria dos tipos" simplesmente é algo totalmente genérico e sem > definição precisa, então não está claro sobre que teoria dos tipos a > pergunta se trata. A definição mais geral razoavel seria , acho, a de pure > type systems ou talvez de logical pure type systems. > > Em terça-feira, 19 de dezembro de 2017, Walter Alexandre Carnielli > <walter.carnie...@gmail.com> escreveu: >> >> Car@s, >> >> >> Isso ja deve ter sido discutido aqui, mas agradeceria se me sugerissem >> >> textos introdutórios sobre Teoria de Tipos, para uso com estudantes >> avancados de >> >> graduação, >> >> >> >> Abraços, >> >> >> Walter >> >> >> >> -- >> Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos >> Grupos do Google. >> Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie >> um e-mail para logica-l+unsubscr...@dimap.ufrn.br. >> Para postar nesse grupo, envie um e-mail para logica-l@dimap.ufrn.br. >> Acesse esse grupo em >> https://groups.google.com/a/dimap.ufrn.br/group/logica-l/. >> Para ver essa discussão na Web, acesse >> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/463F2905-56CA-4EFF-BD41-C002B52F290E%40gmail.com. > > -- > Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos > Grupos do Google. > Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie > um e-mail para logica-l+unsubscr...@dimap.ufrn.br. > Para postar nesse grupo, envie um e-mail para logica-l@dimap.ufrn.br. > Acesse esse grupo em > https://groups.google.com/a/dimap.ufrn.br/group/logica-l/. > Para ver essa discussão na Web, acesse > https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAJGvw-09PdbszQFQ9Bfn0HP8C6kuvkLS1NfDz9Ljagr_9JAm3w%40mail.gmail.com. -- ----------------------------------------------- Walter Carnielli Centre for Logic, Epistemology and the History of Science and Department of Philosophy State University of Campinas –UNICAMP 13083-859 Campinas -SP, Brazil Phone: (+55) (19) 3521-6517 Institutional e-mail: walter.carnie...@cle.unicamp.br Website: http://www.cle.unicamp.br/prof/carnielli CV Lattes : http://lattes.cnpq.br/1055555496835379 -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscr...@dimap.ufrn.br. Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br. Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CA%2Bob58OLUkJH%2Bj9a%2BGAHAhzOMRBp_6sk1qUPpCwiTqXkuRUb-w%40mail.gmail.com.