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 > <https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/463F2905-56CA-4EFF-BD41-C002B52F290E%40gmail.com?utm_medium=email&utm_source=footer> > . > -- 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/CAJGvw-09PdbszQFQ9Bfn0HP8C6kuvkLS1NfDz9Ljagr_9JAm3w%40mail.gmail.com.
