Programa

Lógica Funcional e Teoria da Demonstração

Diploma de Estudos Avançados em Segurança de Informação

Diploma de Estudos Avançados em Matemática

Programa

Cálculo-lambda, teorias, coerência. Redução, formas normais, confluência, teorema de Church-Rosser. Determinadores de pontos-fixos, recursão, definabilidade e computabilidade, tese de Church-Markov-Turing, teorema de Kleene. Resultados de indecidibilidade, teorema de Rice. Lógica combinatória. Tipos simples, redução e normalização. Decidibilidade da tipificação de termos e da verificação de tipos, teorema de Hindley-Milner. O problema da habitação de tipos. Lógicas proposicionais clássica e intuicionista (LPC and LPI), álgebras de Boole e de Heyting, axiomatizações e tertium non datur, correcção e completude. Semântica de Kripke da LPI, propriedade do modelo finito, decidabilidade. Cálculo de sequentes, eliminação do corte, normalização, decidabilidade. A interpretação de Brouwer-Heyting-Kolmogorov da LPI. Habitação de tipos simples e o fragmento implicativo da LPI. O isomorfismo de Curry-Howard, coerência, normalização, decidibilidade da habitação de tipos. Tipos união e produto. Lógica clássica e operadores de controlo. Combinadores, relevância e linearidade. Lógica computacional, fórmulas-como-tipos e provas-como-programas, o lambda-cubo de Barendregt.