Menu Conteúdo Rodapé
  1. Início
  2. Cursos
  3. Engenharia Informática
  4. Teoria da Prova e da Programação

Teoria da Prova e da Programação

Código 14495
Ano 1
Semestre S1
Créditos ECTS 6
Carga Horária OT(15H)
Área Científica Informática
Tipo de ensino presencial
Objectivos de Aprendizagem Esta disciplina visa abordar os tópicos fundamentais da ciência da computação e da programação.

Após a conclusão desta UC, o aluno deverá ser capaz de:
- modelar , formalizar e desenvolver provas por computador
- modelar matematicamente programas
- comprender, definir e extender a semântica de linguagens de programação
- comprender, usar os modelos matemáticos da programação e da prova
Conteúdos programáticos A UC propõe a exposição dos alicerces conceptuais, as técnicas e as ferramentas que permitam explicar, justificar e conceber o raciocínio por computador como também as linguagens de programação e os seus próprios programas, baseando-se neste propósito num contexto teórico abrangente e uniforme.

Lógica Proposicional e Predicativa, Sistemas de dedução, Problemas de decisão
Procedimentos de Decisão clássicos
Sistemas deductivos e Dedução Natural
Lógica Intuicionista e Lógica de Ordem superior
Lambda calculo puro e com tipos
Isomorfismo de Curry Howard
Tipos Dependentes
Semantica operacional
Teoria dos domínios
Semântica Denotacional
Aspectos fundamentais das linguagens de programação
Metodologias de Ensino e Critérios de Avaliação Avaliação teórica : 50% da avaliação global (avaliação de trabalhos de natureza teórica) Avaliação prática: 50% da avaliação global (avaliação de trabalhos de natureza prática)
Bibliografia principal José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa. Rigorous Software Development An Introduction to Program Verification. Springer Verlag, 2010.

Morten Heine B. Sørensen , Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism (1998)


John Harrison. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009.

B. A. Davey and H. A. Priestley. Introduction to Lattices and Order: 2nd Ed.. Cambridge University Press, 2002.

Henk P. Barendregt. Lambda calculi with types. In S. Abramsky, D. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, chapter 2, pages 117?309. Oxford University Press, 1992.

A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory
Cambridge Tracts in Theoretical Computer Science(No. 43)
2nd Edition, 2000.


H. R. Nielson and F. Nielson. Semantics with Applications. John Wiley & Sons, Chichester, 1993
Língua Português
Data da última atualização: 2021-06-24
As cookies utilizadas neste sítio web não recolhem informação pessoal que permitam a sua identificação. Ao continuar está a aceitar a política de cookies.