Grupo de Pesquisa
Investigação de modelos computacionais mais próximos às especificações de implementação, neste caso com a definição explícita da operação de substituição, baseadas nos modelos correspondentes. Os temas abordados, como as propriedade de confluência, terminação e designação de tipos, estão relacionados aos problemas práticos na implementação de linguagens de programação e assistentes de prova de ordem superior tipados.
Estudo das estruturas matemáticas através da álgebra, lógica e teoria de modelos, com aplicações em teoria dos números, e como fundamento em ciência da computação.
Investigação da semântica de processos computacionais através dos sistemas de tipos e sua relação com lógicas.
Utilização da teoria de reescrita, teoria de tipos, lógica nominal e de reescrita na verificação formal de correção de software. Aplicações em teoria de reescrita, criptografia e otimização. Formalização de propriedades de sistemas de reescrita de termos, cálculos de substituições explícitas e sistemas nominais de reescrita.
Estudar a complexidade de problemas envolvendo ordenação de permutações, restrito a determinadas operações; Estudar de que modo algoritmos genéticos podem ser úteis para computar a distância de permutações em relação à permutação identidade, para problemas de rearranjo de genomas que são sabidos ser NP-difíceis; Restritos a uma determinada operação em Sn, o grupo de permutações, estabelecer expressões para o número médio de operações necessárias na ordenação das permutações de Sn.
Investigação da teoria de reescrita, incluíndo a ampla possibilidade de aplicação, como a unificação de ordem superior, especificações de protocolos criptográficos e em projetos de hardware. Desenvolvimento de bibliotecas (teorias) para assistentes de prova que permitam a utilização do arcabouço teórico de reescrita em projetos de formalização.
Investigação dos tipos como fundamento em Matemática e Computação.