Departamento de Informática (UM)

Semântica das Linguagens de Programação

10865 [8506O8]

Licenciatura em Ciências da Computação [CCOM]

S6

Renato Jorge Araújo Neves

Objetivos

Esta UC faz uma introdução à semântica formal das linguagens de programação. Na primeira parte são apresentadas diferentes abordagens (operacional, denotacional e axiomática) à semântica das linguagens imperativas. A segunda parte é dedicada à semântica das linguagens funcionais, tendo o lambda-calculus como núcleo central.

Programa

- A linguagem While: uma linguagem imperativa simples. Semântica das expressões. Diferentes abordagens à semântica da linguagem.
- Semântica operacional (natural e estrutural) para a linguagem While e suas diferentes extensões.
- Uma implementação correta dos programas While numa máquina abstrata.
- Semântica axiomática. Verificação dedutiva de programas While. Correção da Lógica de Hoare.
- Semântica denotacional para a linguagem While.
- Lambda-calculus puro e Lambda-calculus com tipos. Principais conceitos e propriedades. Estratégias de redução.
- Uma linguagem de programação funcional estrita. Sistema de tipos. Semântica de avaliação aplicativa ("call-by-value").
- Uma linguagem de programação funcional não estrita. Sistema de tipos. Semântica de avaliação normal ("call-by-name").

Bibliografia

Nielson, H., Nielson, F. (2007). Semantics with applications: a formal introduction. Springer.

Reynolds, J. C. (1998). Theories of Programming Languages. Cambridge University Press.

Resultados da aprendizagem

- Descrever as características das abordagens operacional, axiomática e denotacional à semântica das linguagens de programação.
- Construir árvores de derivação nos sistemas de inferência definidos pelas diferentes abordagens semânticas.
- Atribuir significado formal aos diferentes aspetos de uma linguagem imperativa ou funcional simples.
- Utilizar técnicas indutivas para argumentar sobre propriedades das linguagens de programação.
- Utilizar o lambda-calculus com modelo de computação e como sistema de reescrita.
- Utilizar sistemas de tipos para regular a boa formação de programas.

Método de avaliação

É adotado o método de avaliação periódica, constando de dois ou mais instrumentos de avaliação, a realizar individualmente ou em grupo. Os alunos que não obtenham aprovação no quadro de avaliação periódica, se cumprirem os requisitos de frequência à UC, caso existam, são admitidos a exame final de recurso.

Funcionamento

Turno: T 1; Docente: Renato Jorge Araújo Neves; Dep.: DI; Horas: 30.
Turno: TP 1; Docente: Renato Jorge Araújo Neves; Dep.: DI; Horas: 30.