A máquina abstracta categorial

Abstract

Desde o trabalho seminal de P. J. Landin nos anos 1960 que se têm utilizado máquinas abstractas para a implementação de linguagens de programação. Nos anos 1980 foi estabelecida uma correspondência entre o Cálculo λ e uma variante da Lógica Combinatória inspirada em categorias cartesianas fechadas. Desta relação surgiu uma máquina abstracta para a implementação do Cálculo λ — a Máquina Abstracta Categorial, ou CAM. Historicamente, esta nova máquina abstracta esteve na origem da linguagem de programação funcional Caml. Nesta dissertação explicamos como surgiu a CAM, exemplificamos o seu uso, demonstramos a sua correcção, e fazemos um enquadramento histórico à sua volta. Complementamos a literatura de referência ao formalizarmos e demonstrarmos correctas três extensões: constantes, condicionais e operador de ponto-fixo.

Since the seminal work of P.J. Landin in the 1960s, abstract machines have been used for the implementation of programming languages. In the 1980s a correspondence has been established between λ-calculus and a variant of Combinatory Logic inspired by cartesian closed categories. From this relationship, an abstract machine has arised for the implementation of λ- calculus — the Categorical Abstract Machine, or CAM. Historically, this new abstract machine led to the functional programming language Caml. In this dissertation it is explained how the CAM emerged, it is illustrated its usage, it is demonstrated its correctness, and it is made an historical insersion. The reference literature is complemented by formalising and demonstrating the correctness of three extensions: constants, conditionals and fixed-point operator.