[pt] Garantir que programas são implementados de forma a cumprir uma especificação é uma questão fundamental em computação, por isso, têm sido propostos vários métodos que almejam provar a correção dos programas. Este trabalho apresenta um método, baseado no isomorfismo de Curry-Howard, que extrai conteúdos computacionais de provas intuicionistas, conhecido como síntese construtiva ou proofs-as-programs. É proposto um processo de síntese construtiva de programas, onde a extração do conteúdo computacional gera um programa em linguagem imperativa a partir de uma prova em lógica intuicionista poli-sortida, cujos axiomas definem os tipos abstratos de dados, sendo utilizado como sistema dedutivo a Dedução Natural. Também é apresentada uma prova de correção, bem como uma prova de completude do método atráves do uso de um sistema com regra ômega (computacional) para a aritmética de Heyting, concluindo com uma demonstração da relação entre o uso da indução finita no lugar da regra ômega computacional no processo de síntese. / [en] One of the main problems in computer science is to assure that programs are implemented in such a way that they satisfy a given specification. There are many studies about methods to prove correctness of programs. This work presents a method, belonging to the constructive synthesis or proofs-as-programs paradigm, that comes from the Curry- Howard isomorphism and extracts the computational contents of intuitionist proofs. The synthesis process proposed produces a program in an imperative language from a proof in many-sorted intuitionist logic, where the axioms define the abstract data types using Natural Deduction as deductive system. It is proved the correctness, as well as the completeness of the method regarding the Heyting arithmetic with ômega-rule(in its computational version). A discussion about the use of the finitary induction instead of computational ômega-rule concludes the work.

[pt] Esta dissertação investiga o uso de programação genética linear na síntese automática de programas em linguagem de montagem para microcontroladores, que implementem estratégias de controle de tempo ótimo ou sub-ótimo, do sistema a ser controlado, a partir da modelagem matemática por equações dinâmicas. Uma das dificuldades encontradas no projeto convencional de um sistema de controle ótimo é que soluções para este tipo de problema normalmente implicam em uma função altamente não-linear das variáveis de estado do sistema. Como resultado, várias vezes não é possível encontrar uma solução matemática exata. Já na implementação, surge a dificuldade de se ter que programar manualmente o microcontrolador para executar o controle desejado. O objetivo deste trabalho foi, portanto, contornar tais dificuldades através de uma metodologia que, a partir da modelagem matemática de uma planta, fornece como resultado um programa em linguagem de montagem. O trabalho consistiu no estudo sobre os possíveis tipos de representações para a manipulação genética de programas em linguagem de montagem, tendo sido concluído que a linear é a mais adequada, e na implementação de uma ferramenta para realizar os três estudos de caso: water bath, cart centering e pêndulo invertido. O desempenho de controle dos programas sintetizados foi comparado com o dos sistemas obtidos por outros métodos (redes neurais, lógica fuzzy, sistemas neurofuzzy e programação genética). Os programas sintetizados demonstraram, no mínimo, o mesmo desempenho, mas com a vantagem adicional de fornecerem a solução já no formato final da plataforma de implementação escolhida: um microcontrolador. / [en] This dissertation investigates the use of genetic programming in automatic synthesis of assembly language programs for microcontrollers, which implement time-optimal or sub-optimal control strategies of the system to be controlled, from the mathematical modeling by dynamic equations. One of the issues faced in conventional design of an optimal control system is that solutions for this kind of problem commonly involve a highly nonlinear function of the state variables of the system. As a result, frequently it is not possible to find an exact mathematical solution. On the implementation side, the difficulty comes when one has to manually program the microcontroller to run the desired control. Thus, the objective of this work was to overcome these difficulties applying a methodology that, starting from the mathematical modeling of a plant, provides as result an assembly language microcontroller program. The work included a study of the possible types of genetic representation for the manipulation of assembly language programs. In this regard, it has been concluded that the linear is the most suitable representation. The work also included the implementation of a tool to accomplish three study cases: water bath, cart centering and inverted pendulum. The performance of control of the synthesized programs was compared with the one obtained by other methods (neural networks, fuzzy logic, neurofuzzy systems and genetic programming). The synthesized programs achieved at least the same performance of the other systems, with the additional advantage of already providing the solution in the final format of the chosen implementation platform: a microcontroller.