Textos introdutórios sobre Teoria de Tipos

[Walter Alexandre Carnielli]

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

[Thanos Tsouanas]

Oi Walter,

On Tue, Dec 19, 2017 at 06:07:12PM -0200, Walter Alexandre Carnielli wrote:
> 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,

https://github.com/jozefg/learn-tt


Abraço

--
Thanos
http://www.tsouanas.org/

[Walter Alexandre Carnielli]

Muito obrigado, Thanos!

Abracos,
Walter

> --
> 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+u...@dimap.ufrn.br.
> Para postar neste grupo, envie um e-mail para logi...@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/20171219201640.GA27051%40necroulis.the.undead.host.

[Carlos Gonzalez]

Impressionante esse site.

Muito obrigado Thanos!

Carlos

--
Thanos
http://www.tsouanas.org/

--
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+unsubscribe@dimap.ufrn.br.

[Fernando Yamauti]

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.

--
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+unsubscribe@dimap.ufrn.br.

Para postar nesse grupo, envie um e-mail para logi...@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.

[Walter Carnielli]

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
<fgya...@gmail.com> escreveu:

>> um e-mail para logica-l+u...@dimap.ufrn.br.

>> Para postar nesse grupo, envie um e-mail para logi...@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+u...@dimap.ufrn.br.

> Para postar nesse grupo, envie um e-mail para logi...@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.c...@cle.unicamp.br

Website: http://www.cle.unicamp.br/prof/carnielli
CV Lattes : http://lattes.cnpq.br/1055555496835379