Dados Gerais do Componente Curricular
| Tipo do Componente Curricular: |
DISCIPLINA |
| Unidade Responsável: |
PROGRAMA DE PÓS-GRADUAÇÃO EM MATEMÁTICA APLICADA E ESTATÍSTICA (12.51) |
| Curso: |
MESTRADO EM MATEMÁTICA APLICADA E ESTATÍSTICA/PPGMAE - NATAL |
| Código: |
PGMAE0030 |
| Nome: |
SISTEMAS DE TIPOS E PROVAS FORMAIS |
| Carga Horária Teórica: |
60 h. |
| Carga Horária Prática: |
0 h. |
| Carga Horária Total: |
60 h. |
| Pré-Requisitos: |
|
| Co-Requisitos: |
|
| Equivalências: |
|
| Excluir da Avaliação Institucional: |
Não |
| Matriculável On-Line: |
Sim |
| Método de Avaliação: |
CONCEITO |
| Horário Flexível da Turma: |
Não |
| Horário Flexível do Docente: |
Sim |
| Obrigatoriedade de Nota Final: |
Sim |
| Pode Criar Turma Sem Solicitação: |
Não |
| Necessita de Orientador: |
Não |
| Exige Horário: |
Sim |
| Permite CH Compartilhada: |
Não |
| Permite Múltiplas Aprovações: |
Não |
| Quantidade de Avaliações: |
1 |
| Ementa/Descrição: |
Cálculo lambda, cálculo lambda simplesmente tipado, isomorfismo Curry–Howard, sistemas de segunda ordem, tipos dependentes, cálculo de construções, lógica no cálculo de construções, provadores de teoremas, especificações e verificação de sistemas, formalização de provas matemáticas. |
| Referências: |
1. Rob Nederpelt and Herman Geuvers. Type Theory and Formal Proof - An Introduction. Cambridge University Press. 2014.
2. Benjamin C. Pierce. Types and programming languages. MIT Press 2002
3. A. Troelstra, H. Schwichtenberg. Basic Proof Theory. Cambridge University Press, 2000.
4. Benjamin C. Pierce, Chris Casinghino, et at. Software Foundations. 2015
5. Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development. Springer, 2004.
|
|
|
