Horário de Atendimento
–2a.fa., entre as 14:30 e as 17:30
–4a.fa., entre as 14:30 e as 17:30
Semântica da Programação – LCC, 3o. ano
Programa Resumido
–Estudo de uma linguagem imperativa simples:
* Definição
* Provas por indução
* Semântica operacional: semântica de transições (estrutural, ou small-step) e semântica de avaliação (natural, ou big-step)
* Equivalência semântica
* Semântica axiomática (breve referência)
–O λ-calculus:
* Definição
* Redução, igualdade e normalização
* Codificação de dados (breve referência)
* Definição de funções recursivas
* O sistema de tipos simples. Tipos intrínsecos e extrínsecos
* Estudo de uma linguagem de programação estrita. Semântica de avaliação
* Estudo de uma linguagem de programação não-estrita. Semântica de avaliação
–Semântica denotacional (introdução)
–Outros tópicos:
* Notas sobre linguagens realistas com características imperativas e funcionais (ISWIM, ALGOL)
* Tratamento semântico dos arrays
Bibliografia de Apoio
LIVROS
–Reynolds, J.C. Theories of Programming Languages. Cambridge Univ. Press, 1998
–Winskel, G. The Formal Semantics of Programming Languages. MIT Press, 1993
–Hennessy, M. The Semantics of Programming Languages. Wiley, 1990
[ versão disponível online aqui ]
TEXTOS
–Pitts A. M. Lecture Notes on Semantics of Programming Languages. Univ Cambridge, 1997-2002
–Mycroft A. Foundations of Functional Programming. Univ. Cambridge, 2007
–Winskel F. Lecture Notes on Denotational Semantics. Univ. Cambridge, 1997-2002
Avaliação
Os alunos poderão optar entre:
–avaliação por exame final
–avaliação periódica, sendo:
* a 1a. parte da matéria avaliada num teste a ter lugar na semana de 7 de Maio
* a 2a. parte da matéria avaliada no exame final