Ferramentas de Utilizador

Ferramentas de Site


inf05516:homepage

:!: Página descontinuada, provavelmente o material não é mais acessível.

Semântica formal N (2006/2)

If you don't have a specification, it can't be wrong.
It can only be surprising.

:!: Bem-vindo à semântica.

Informações gerais

Carga horária: 60 h (em 30 aulas de 2h)
Créditos: 4
Súmula: Introdução ao cálculo lambda. Domínios de Scott; pontos fixos de funções contínuas. Semântica denotacional. Semântica algébrica. Semântica de ações. Semântica axiomática. Semântica operacional.
Turma: U
Horário/Sala: Segunda 08:30-10:10 e quarta 08:30-10:10 na sala 108 do prédio 43425 (vê também aqui).
Consultas: Quarta 15-17.
Detalhes: Vê o programa.

Resultados

Materiais

Aulas

No. Data Tópicos Handout Exercícios Soluções Leitura
1 07/08 Administrativa. Introdução. 1a 1b NN1
2 09/08 A linguagem Arith. Semântica operacional e denotational. 2 NN1
3 14/08 Semântica operacional natural da linguagem IMP. 3 1 1 NN2.1
4 16/08 Princípios de indução e características de linguagens. 4 NN2.1,W3.3
5 21/08 Características de linguagens. 5 2 2 NN2.1,W3.4,W4
6 23/08 Semântica operacional estrutural da linguagem IMP. 6 NN2.2
7 28/08 Introdução a OCaml. 7 3 3 OCaml
8 30/08 IMP em OCaml. Introdução ao cálculo lambda. 8 P5
9 04/09 Estrategias de avaliação no cálculo lambda. Escopos em IMP. (material de 8,10) 4 4 P5
10 06/09 Escopos, declarações, introdução em sistemas de tipos. 10 P1
11 11/09 Extensões de IMP: Variáveis booleanas. 11
12 13/09 Extensões de IMP: Constantes, procedimentos. 12 5 5
13 18/09 Extensões de IMP. (material de 12)
20/09 Feriado: Revolução Farroupilha Entrega dos exercícios: 21/09
14 25/09 Revisão é exercícios unidade 1.
15 27/09 Prova 1 P1 SP1
16 02/10 Semântica axiomática: Introdução. 16 HR4.1-3
17 04/10 Semântica axiomática: Condicional, laços. 17 HR4.3
18 09/10 Semântica axiomática: Corretude total, exemplos. 18 6 6 HR4.4
19 11/10 Revisão prova 1 (soluções SP1 acima).
20 16/10 Semântica denotational: Introdução. 19 R2.1,2.2
21 18/10 Semântica denotational: Laços. 21 7 7 R2.2
22 23/10 Semântica denotational: Laços. 22 R2.2
23 25/10 Semântica denotational: Teorema do ponto fixo. Teoria de domínios. (Material 22) R2.3,2.4
24 30/10 Semântica denotational: Teorema do ponto fixo. Aplicação a IMP. 24 R2.3,2.4
25 01/11 Semântica denotational: Exercícios. (Material 24) 8 8 R2.5
26 06/11 Semântica denotational: Extensões. 26
27 08/11 Revisão: Semâtica axiomática e denotational. Entrega dos exercícios
28 13/11 Prova 2 P2 SP2
15/11 Feriado: Proclamação da República.
29 20/11 Apresentação de trabalhos.
30 22/11 Apresentação de trabalhos.
11/12 Aula de revisão R1 SR1
13/12 Prova de recuperação PR SPR
15/12 Término oficial das aulas.
  • Observação: Os exercícios devem ser entregados até uma semana antes da prova.
  • Abreviações dos livros: NN=Nielson e Nielson, W=Winskel, P=Pierce, HR=Huth/Ryan, R=Reynolds

Suplementos

  • Padrão da linguagem Scheme, em particular secção 7.2 sobre “Formal semantics”
  • Padrão (antiga) da linguagem C++ (uso restrito: escreve email)

Bibliografia

Locations of visitors to this page

inf05516/homepage.txt · Esta página foi modificada pela última vez em: 2010/01/18 15:45 (Edição externa)