Concepção de sistemas de reescrita condicionais com premissas gerais e não puramente equacionais como é o caso usual. Comparação entre cálculos de substituições explícitas e análise da aplicabilidade prática destes cálculos em problemas como por exemplo a adatação do cálculo de substituições explícitas lambda s_e para tratar a unificação e matching de ordem superior.Desenvolvimento de uma metodologia baseada em reescrita-lógica para especificação e verificação de hardware reconfigurável.Aplicações de métodos formais nos sistemas PVS e Coq, que incluim gerenciamento de tráfego aéreo, criptografia e algoritmos algébricos. Destaca-se a formalização de uma teoria de sistemas de reescrita de termos no asistente de demonstração PVS, denominada trs e disponível na livraria PVS do NASA LaRC. Desenvolvimento e formalização de técnicas equacionais para unificação, estreitamento e verificação de identidades em arcabouços de substituições explícitas e sistemas nominais.
