De occam para o transputer: compilação via reescrita de termos - Spencer, Renata; Sampaio, Augusto (Anais do Simpósio Brasileiro de Engenharia de Software (SBES); 1996: Anais do X Simpósio Brasileiro de Engenharia de SoftwareDO - 10.5753/sbes.1996.24440, 1996)
The aim of this work is the development of a prototype compiler from occam to the transputer, in such a way that the correctness of the compiler is ensured by construction. The method used reduces the source program, through a series of algebraic transformations, to a normal form which can be directly mapped into the instructions of the target machine. Using the term rewriting facilities provided by OBJ3, the correctness proof gives as a byproduct a compiler prototype, so that at the end of the process, a running prototype will be available. This compilation method was already available, and its application was illustrated for a very simple language; our purpose here is to extend the method to deal with realistic languages and machines, such as occam and the transputer.