Estruturas Formais, Fundamentos e Aplicações

Grupo de Pesquisa

Linhas de Pesquisa

Cálculos de substituições explícitas e aplicações

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.

Estruturas Algébricas e Aplicações

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.

Lógica e Semântica da Computação

Investigação da semântica de processos computacionais através dos sistemas de tipos e sua relação com lógicas.

Métodos Formais em Computação

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.

Ordenação de permutações e aplicações

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.

Teoria de Reescrita e Aplicações

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.

Teoria de Tipos

Investigação dos tipos como fundamento em Matemática e Computação.