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
|