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