Índice

Notas

(Inclui já notas do exame)

Aqui

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

Material de Apoio

• Slides (serão actualizados ao longo do semestre)

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
• 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 20%
• teste ou exame, com peso de 80%

-- JorgeSousaPinto - 09 Mar 2009