Índice

Notas

• Notas práticas e Teste
• Notas Exame e Finais

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

• O λ-calculus:
  • Definição
  • Redução, igualdade e normalização
  • 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

• Introdução à semântica denotacional

• Outros tópicos
  • Notas sobre linguagens realistas com características imperativas e funcionais (ISWIM, ALGOL)
  • Tratamento semântico dos arrays

Bibliografia

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 (disponível online aqui)

Textos

• Pitts A. M. Lecture Notes on Semantics of Programming Languages. Univ Cambridge, 1997-2002 (disponível online aqui)
• Mycroft A. Foundations of Functional Programming. Univ. Cambridge, 2007
• Winskel F. Lecture Notes on Denotational Semantics. Univ. Cambridge, 1997-2002

Avaliação

Terá as seguintes componentes:

• periódica, nas aulas TP, com peso de 30%
• teste ou exame, com peso de 70% (nota mínima 8 valores)

-- JorgeSousaPinto - 02 Mar 2010