|
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
|
|
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
|