:!: 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 [[http://www.inf.ufrgs.br/cei/nscad/images/stories/mapa.jpg|prédio 43425]] (vê também [[http://www1.ufrgs.br/Graduacao/InformacoesAcademicas/horariosvagasdepto.asp?act=showtable&cboDepartamento=705&cboSemestre=2006012|aqui]]).\\ **Consultas:** Quarta 15-17.\\ **Detalhes:** Vê o {{:inf05516:programa.pdf|programa}}. ===== Resultados ===== * :!: [[inf05516-2006-1-F|Frequência]] * Frequência [[inf05516-2007-1-FA|Turma A]], [[inf05516-2007-1-FB|Turma B]] * [[inf5516-2006-1-Notas|Notas]] * [[inf5516-2006-2-Trabalhos|Trabalhos]] ===== Materiais ===== * [[http://www.inf.ufrgs.br/~afmoreira/Semantica/index.html|Página da disciplina]] por [[http://www.inf.ufrgs.br/~afmoreira|Álvaro Freitas Moreira]]. * [[:inf05516|Minha página da disciplina em 2006/1]]. ==== Aulas ==== ^ No. ^ Data ^ Tópicos ^ Handout ^ Exercícios ^ Soluções ^ Leitura ^ | 1 | 07/08 | Administrativa. Introdução. | {{s01a.pdf|1a}} {{s01b.pdf|1b}} | | | NN1 | | 2 | 09/08 | A linguagem Arith. Semântica operacional e denotational. | {{s02.pdf|2}} | | | NN1 | | 3 | 14/08 | Semântica operacional natural da linguagem IMP. | {{a02.pdf|3}} | {{e01.pdf|1}} | {{so01a.pdf|1}} | NN2.1 | | 4 | 16/08 | Princípios de indução e características de linguagens. | {{a03.pdf|4}} | | | NN2.1,W3.3 | | 5 | 21/08 | Características de linguagens. | {{a04.pdf|5}} | {{e02.pdf|2}} | {{so02.pdf|2}} | NN2.1,W3.4,W4 | | 6 | 23/08 | Semântica operacional estrutural da linguagem IMP. | {{a05.pdf|6}} | | | NN2.2 | | 7 | 28/08 | Introdução a OCaml. | {{a06.pdf|7}} | {{e03.pdf|3}} | {{so03.pdf|3}} | [[:ocaml|OCaml]] | | 8 | 30/08 | IMP em OCaml. Introdução ao cálculo lambda. | {{a07.pdf|8}} | | | P5 | | 9 | 04/09 | Estrategias de avaliação no cálculo lambda. Escopos em IMP. | (material de 8,10) | {{e04a.pdf|4}} | {{so04a.pdf|4}} | P5 | | 10 | 06/09 | Escopos, declarações, introdução em sistemas de tipos. | {{a08a.pdf|10}} | | | P1 | | 11 | 11/09 | Extensões de IMP: Variáveis booleanas. | {{a09.pdf|11}} | | | | | 12 | 13/09 | Extensões de IMP: Constantes, procedimentos. | {{a09a.pdf|12}} | {{e05a.pdf|5}} | {{so05a.pdf|5}} | | | 13 | 18/09 | Extensões de IMP. | (material de 12) | | | | | | 20/09 | **Feriado:** [[wppt>Guerra_dos_Farrapos|Revolução Farroupilha]] | **Entrega dos exercícios: 21/09** | | | | | 14 | 25/09 | Revisão é exercícios unidade 1. | | | | | | 15 | 27/09 | **Prova 1** | | {{p01a.pdf|P1}} | {{sp01a.pdf|SP1}} | | | 16 | 02/10 | Semântica axiomática: Introdução. | {{a10.pdf|16}} | | | HR4.1-3 | | 17 | 04/10 | Semântica axiomática: Condicional, laços. | {{a11.pdf|17}} | | | HR4.3 | | 18 | 09/10 | Semântica axiomática: Corretude total, exemplos. | {{a12.pdf|18}} | {{e05.pdf|6}} | {{s05.pdf|6}} | HR4.4 | | 19 | 11/10 | Revisão prova 1 (soluções SP1 acima). | | | | | | 20 | 16/10 | Semântica denotational: Introdução. | {{a19.pdf|19}} | | | R2.1,2.2 | | 21 | 18/10 | Semântica denotational: Laços. | {{a20.pdf|21}} | {{e08.pdf|7}} | {{s08.pdf|7}} | R2.2 | | 22 | 23/10 | Semântica denotational: Laços. | {{a21.pdf|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. | {{a22.pdf|24}} | | | R2.3,2.4 | | 25 | 01/11 | Semântica denotational: Exercícios. | (Material 24) | {{e09.pdf|8}} | {{s09.pdf|8}} | R2.5 | | 26 | 06/11 | Semântica denotational: Extensões. | {{a23.pdf|26}} | | | | | 27 | 08/11 | Revisão: Semâtica axiomática e denotational. | **Entrega dos exercícios** | | | | | 28 | 13/11 | **Prova 2** | | {{p02b.pdf|P2}} | {{sp02b.pdf|SP2}} | | | | 15/11 | **Feriado**: [[wppt>Proclamação_da_República_Brasileira|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 | | {{er1.pdf|R1}} | {{sr1.pdf|SR1}} | | | | 13/12 | **Prova de recuperação** | | {{p02c.pdf|PR}} | {{sp02c.pdf|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 ==== * [[http://www.schemers.org/Documents/Standards/R5RS/r5rs.pdf|Padrão]] da linguagem Scheme, em particular secção 7.2 sobre "Formal semantics" * Padrão (antiga) da linguagem C++ (uso restrito: escreve email) * [[OCaml|Material sobre OCaml]] ==== Bibliografia ==== Locations of visitors to this page