Synopses & Reviews
Synopsis
O calculo lambda e um dos pilares da ciencia da computacao. Para alem
do seu papel historico em teoria da computabilidade, teve influencia
significativa no desenho e implementacao de linguagens de programacao,
em semantica denotacional, e em teoria de dominios. O livro da enfase
a teoria da demonstracao do calculo lambda sem tipos. Os primeiros
capitulos concentram-se neste calculo e abordam a teoria basica,
reducoes, modelos, computabilidade e o relacionamento entre o calculo
lambda e a logica combinatoria. O Capitulo 7 introduz o calculo lambda
com tipos: primeiro o calculo lambda simplesmente tipificado, de
seguida com o polimorfismo a Milner e, por ultimo, o calculo lambda
polimorfico. O Capitulo 9 apresenta versoes mais recentes do calculo
lambda sem tipos: o calculo lambda preguicoso e o calculo lambda
sigma. O ultimo capitulo contem referencias e um guia para leitura
ulterior. Os exercicios vao sendo propostos ao longo do livro. Em
contraste com livros anteriores sobre estes topicos, que foram
escritos por logicos, este livro e escrito do ponto de vista da
ciencia da computacao e realca o significado pratico de muitas das
ideias chave. O livro assume-se como livro de texto para o ultimo ano
de graduacao ou para o primeiro ano de pos-graduacao em ciencia da
computacao. Os estudantes de investigacao poderao usa-lo como uma
introducao a literatura mais especializada da area.