Fundamentos da programação lógica e funcional: o princípio de resolução e a teoria de reescrita

Um dos aspectos mais relevantes da ciência da computação é o desenvolvimento de arcabouços matemáticos robustos para a implementação de novas linguagens de computação. Ainda que as primeiras linguagens de programação tenham sido desenvolvidas com téc nicas ad hoc, definidas por restrições de hardware, em meados do século XX, os pilares dessa tecnologia foram elaborados no início desse século. Matemáticos como Alonzo Church e Alan Turing , trabalhando em fundamentos da computação relacionados com a própria noção de computabilidade, elaboraram modelos computacionais como as máquinas de Turing e o cálculo lambda, modelos sob os quais importantes questões sobre os fundamentos matemáticos e da semântica da computação foram respondidas. São os fun damentos semânticos da computação o foco central desta obra, necessários tanto para a compreensão das linguagens computacionais modernas quanto para o desenvolvimento formal de novos paradigmas aplicados na elaboração de novas linguagens de programaç ão e linguagens de especificação e verificação formal. A obra é proposta como notas de aula para um curso avançado complementar em teoria da computação, do ponto de vista dos formalismos lógicos e semânticos. Ainda que a obra restrinja-se aos fundame ntos matemáticos dos paradigmas de programação lógica e funcional, fornece os elementos necessários para iniciar um aprofundamento em áreas de investigação centrais em computação, envolvidas no desenvolvimento tecnológico de novas linguagens computac ionais, como são a própria teoria de reescrita, a teoria de tipos e a teoria de prova. Certamente, alunos de pós-graduação e em estágios avançados de cursos em áreas tecnológicas e exatas, como Ciência da Computação, Matemática, Informática e Engenha rias de Software, Computação, Automação e Mecatrônica, poderão aproveitar bem esta obra.