Introducao Ao Calculo Lambda

O clculo lambda um dos pilares da cincia da computao. Para almdo seu papel histrico em teoria da computabilidade, teve influnciasignificativa no desenho e implementao de linguagens de programao,em semntica denotacional, e em teoria de domnios. O livro d nfase teoria da demonstrao do clculo lambda sem tipos. Os primeiroscaptulos concentram-se neste clculo e abordam a teoria bsica,redues, modelos, computabilidade e o relacionamento entre o clculolambda e a lgica combinatria. O Captulo 7 introduz o clculo lambdacom tipos: primeiro o clculo lambda simplesmente tipificado, deseguida com o polimorfismo Milner e, por ltimo, o clculo lambdapolimrfico. O Captulo 9 apresenta verses mais recentes do clculolambda sem tipos: o clculo lambda preguioso e o clculo lambdasigma. O ltimo captulo contm referncias e um guia para leituraulterior. Os exerccios vo sendo propostos ao longo do livro. Emcontraste com livros anteriores sobre estes tpicos, que foramescritos por lgicos, este livro escrito do ponto de vista dacincia da computao e reala o significado prtico de muitas dasideias chave. O livro assume-se como livro de texto para o ltimo anode graduao ou para o primeiro ano de ps-graduao em cincia dacomputao. Os estudantes de investigao podero us-lo como umaintroduo literatura mais especializada da rea.