Fundamentos da Computação

Lógicas Não Clássicas em Coq
Produzir software confiável não é uma tarefa simples. Dentre os métodos utilizados para este fim encontra-se autilização de ferramentas para especificar e raciocinar sobre propriedades desejadas do software em questão. Neste sentido, assistentes de provas são empregados para modelar sistemas e provar sua corretude. Coq é um assistente de provas largamente utilizado e com diversas funcionalidades que auxiliam na tarefa de produção de software confiável. Por outro lado, sistemas lógicos são necessários para especificar e modelar formalmente tais aspectos de software. Existe uma gama vasta de sistemas lógicos, cada qual captura um tipo diferente de aspectos a serem modelados. Desta forma, para ampliar o uso de assistentes de prova em um maior contingente de expressividade de propriedades de software, faz-se necessária a formalização de diferentes sistemas lógicos dentro de tais assistentes. O objetivo principal deste projeto é formalizar sistemas lógicos não clássicos dentro do assistente de provas Coq.

Sistemas de Tipos para Linguagens de Programação
O uso de tipos em linguagens de programação tem objetivos diversos, como a detecção de erros, a definição de abstrações, a otimização do código gerado e a documentação de programas. Também existem linguagens recentes, como por exemplo Agda, Idris e Coq, que foram projetadas com sistemas de tipos dependentes que permitem a verificação de propriedades do programa e em alguns casos podem garantir que um programa sempre termina. Linguagens que adotam a verificação de tipos em tempo de compilação são classificadas como linguagens com tipagem estática, por exemplo Haskell, SML e C. Enquanto linguagens com tipagem dinâmica abrem mão dessa verificação de tipos em tempo de compilação, visando maior flexibilidade na codificação. Como, por exemplo, LISP, Scheme e Python. O custo dessa flexibilidade é um processo de depuração mais demorado, uma vez que erros de tipos são detectados apenas em tempo de execução, e velocidade de execução muito inferior, uma vez que as possibilidades de otimizações são extremamente reduzidas e existe o overhead associado a verificação de tipos durante a execução.
O objetivo desse projeto é investigar e propor extensões a sistemas de tipos que permitam maior flexibilidade as linguagens com tipagem estática, aproximando da flexibilidade encontrada nas linguagens com tipagem dinâmica, sem abrir mão da segurança que a tipagem estática proporciona. Permitindo uma codificação de programas mais concisa e códigos genéricos, que aceitem dados de vários tipos.  Um objetivo secundário é estudar o uso de linguagens com tipos dependentes como ferramenta para provar as propriedades dos algoritmos de verificação ou inferência de tipos propostos.