Revisão Provas III e IV

Caros -- quem quiser revisar as provas 3 e 4, por favor me mande uma mensagem, que marcamos um horário!

Novidades

09/05 -- conceitos finais disponíveis. como não há conceito F, nào haverá exame. Boas Férias!
09/05 -- conceitos do T4 e contabilização da L4
05/05 -- notas de aula, versão 31, disponíveis
26/04 -- conceitos do T3 disponíveis
19/04 -- notas de aula, versão 30, disponíveis
17/04 -- notas de aula, versão 29, disponíveis
15/04 -- notas de aula, versão 28, disponíveis
10/04 -- Lista IV atualizada (o exercício 2 tinha problemas)
06/04 -- Lista IV disponível
05/04 -- notas de aula, versão 27, disponíveis
30/03 -- Conceitos do T2 e contabilização de L2 e L3
29/03 -- notas de aula, versão 26, disponíveis
29/03 -- notas de aula, versão 25, disponíveis
28/03 -- notas de aula, versão 24, disponíveis
27/03 -- notas de aula, versão 23, disponíveis
26/03 -- notas de aula, versão 22, disponíveis
24/03 -- notas de aula, versão 21, disponíveis (19 e 20 não existiram)
22/03 -- notas de aula, versão 18, disponíveis
19/03 -- notas de aula, versão 17, disponíveis
16/03 -- Lista III ligeiramente modificada (peguem de novo)
15/03 -- notas de aula, versão 16, disponíveis
14/03 -- Lista III disponível
14/02 -- notas de aula, versão 15, disponíveis
11/03 -- Prazo da Lista II adicionado
10/03 -- Conceitos do T1 e contabilização da L1
09/03 -- notas de aula, versão 14, disponíveis
08/03 -- notas de aula, versão 13, disponíveis
08/03 -- notas de aula, versão 12, disponíveis
07/03 -- notas de aula, versão 11, disponíveis
02/03 -- notas de aula, versão 10, disponíveis
01/03 -- notas de aula, versão 9, disponíveis
26/02 -- notas de aula, versão 8, disponíveis
25/02 -- notas de aula, versão 7, disponíveis
24/02 -- notas de aula, versão 6, disponíveis
24/02 -- Lista II disponível
23/02 -- notas de aula, versão 5, disponíveis
23/02 -- data de entrega da Lista I disponível (29/02)
23/02 -- datas das avaliações disponíveis
22/02 -- notas de aula, versão 4, disponíveis
18/02 -- notas de aula, versão 3, disponíveis -- agora com versão com 
         margens pequenas, para leitura em tela
18/02 -- Lista I disponível
17/02 -- notas de aula, versão 2, disponíveis
17/02 -- notas de aula, versão 1, disponíveis
16/02 -- notas de aula, versão 0, disponíveis
15/02 -- início do curso

Ementa

Semântica Operacional: estrutural e natural. Semântica Denotacional. Semântica Axiomática. Aplicação em demonstração de corretude. Noções rudimentares de semântica de programas concorrentes.

Requisitos

Programação Orientada a Objetos; Lógica Básica; Linguagens Formais e Automata

Informalmente: gosto por linguagens de programação, e sua descrição de forma abstrata.

Avaliação

Quatro provas, valendo 3 cada. Cada prova pode valer exatamente 0, 1, 2 ou 3.
Listas de exercícios, que valerão 0, 1 ou 2 na nota final.

O conceito final será dado pela regra a seguir:

n ∈ [0, 6)→F
n ∈ [6, 8)→C
n ∈ [8, 11)→B
n ∈ [11, 14]→A

Prova substitutiva

Somente para os casos previstos em lei!

Caso o aluno perca uma das provas e apresente justificativa, poderá fazer uma substitutiva no final do quadrimestre.

Exame

Alunos com conceito F terão direito a exame, valendo 14. O conceito final, neste caso, será dado pela mesma regra para as notas, mas usando (8n + 6e)/14 ao invés de n.

Datas das avaliações

P₁: ~~02/03, 19:30~~
P₂: ~~23/03, 19:30~~
P₃: ~~13/04, 19:30~~
P₄: ~~04/05, 19:30~~
S: ~~09/05, 21:00~~
~~E: 16/05, 21:00~~ (ninguém com F!)

Exercícios

Lista I prazo: 29/02
Lista II prazo: 16/03
Lista III prazo: 23/03
Lista IV

Conceitos

Aqui!

Programa

Este programa está sujeito a mudanças simples. Grandes mudanças não devem acontecer.

Revisão-relâmpago de linguagens formais

Conceitos preliminares: sintaxe abstrata; notação a ser usada; indução estrutural.

Uma linguagem-exemplo

Semântica denotacional

Semântica operacional (natural)

Semântica operacional (estrutural)

Semântica axiomática

λ-cálculo sem tipos

λ-cálculo tipado

Concorrência

Bibliografia

Principal

Notas de aula -- o curso seguirá principalmente estas notas.

Alguns livros relativamente fáceis:

Nielson, H. R., Nielson, F. Semantics with Applications: An Appetizer. Springer, 2007. [ 005.131 NIELse ]
- Versão digital via SpringerLink
Stump, A. Programming Language Foundations. Wiley, 2014. ( 978-1-118-00747-1 )
Winskel, G. Formal Semantics of Programming Languages. MIT Press, 1993. [ 005.131 WINSfo ] -- um pouco desatualizado, mas bom.

Cobrindo apenas semântica operacional há o livro de Maribel Fernández:

Fernandez, M. Programming Languages and Operational Semantics: An Introduction. College Publications, 2004. [ 005.13 FERp ]

Cobrindo apenas semântica denotacional há também o livro de Lloyd Allison -- infelizmente não temos na biblioteca (e vocês podem fazer o curso tranquilamente sem ele, sem problemas):

Allison, L. A Practical Introduction to Denotational Semantics. Cambridge, 1987.

Secundária

O λ-cálculo não mudou nos últimos 30 anos. Já a descrição da semantica de linguagens sim, passou por mudanças. Assim, exceto para o que diz respeito ao λ-cálculo, os livros novos podem trazer formulações diferentes (e melhores) que as dos antigos.

Reynolds, J. Theories of Programming Languages Cambridge, 1998. [ 005 REYt ]
Gunter, C. A. Semantics of Programming Languages: Structures and Techniques. MIT Press, 1992.a [ 005.13 GUNs ]. Mais denso, um pouco antigo, mas muito bom.
Dowek, Gilles; Lévy, Jean-Jacques. Introduction to the Theory of Programming Languages. Springer, 2011. ( ISBN: 978-0-85729-075-5 ).
- PDF disponível na rede da UFABC.
Turbak, F., Gifford, D., Sheldon, M. A. Design Concepts in Programming Languages. MIT Press, 2008 [ 005.1 TURd ]
Pierce, B. Types and Programming Languages. MIT Press, 2002. [ 005.13 PIEt ]
Queinnec, C. Lisp in Small Pieces. Cambridge, 1996. [ 005.133 QUEL ] O Capítulo 5 trata de Semântica Denotacional.
Harper, R. Practical Foundations for Programming Languages. Cambridge, 2012.
- versão preliminar online
Mitchell, J.C. Foundations for Programming Languages. MIT Press, 1991.
Stoy, J. E. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, 1981.
Gordon, M. J. C. The Denotational Description of Programming Languages: An Introduction. Springer, 1979/1984 (aparentemente reimpresso em 2013).
Slonneger, K.; Kurtz, B. Formal Syntax and Semantics of Programming Languages. Addison-Wesley, 1995.
Agha, G. A., Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press 1985.
Roscoe, A. W. The Theory and Practice of Concurrency. Prentice Hall, 1997.
Roscoe, A. W. Understanding Concurrent Systems. Springer, 2010.
- PDF Disponível na UFABC
Hoare, C. A. R. Communicating Sequential Processes. Prentice Hall, 2004 (1985).
Milner, R. Communication nad Concurrency. Prentice Hall, 1989. ( ISBN: 0-13-117984-9 )
Schneider, F. B. On Concurrent Programming. Springer, 2007.
Barendregt, H. The Lambda Calculus. Its Syntax and Semantics. College Publications, 2012.
Barendregt, H. Dekkers, W.; Statman, R., Lambda Calculus with Types. Cambridge, 2013.
Hankin, C. An Introduction to Lambda Calculi for Computer Scientists. College Publications, 2004.
Hüttel, H. Transitions and Trees: An Introduction to Structural Operational Semantics. Cambridge, 2010.
Caromel, D; Henrio, L. A Theory of Distributed Objects. Springer, 2005 [ 519.24 CAROth ] Também disponível em formato digital na UFABC
Stoltenberg-Hansen, Viggo; Lindström, Ingrid; Girffor, Edward R. Mathematical Theory of Domains. Camridge, 1994. ( ISBN: 978-521-06479-8 ) -- Sobre Teoria de Domínios, só para quem gostar.
Fiore. M. Axiomatic domain theory in categories of partial maps. Cambridge, 1996, ( ISBN: 0-521-60277-7 ). Para Matemáticos com interesse em Categorias.
Abramsky, S; Jung, A (1994). Domain theory (PDF). Em S. Abramsky, D. M. Gabbay, T. S. E. Maibaum (editores), Handbook of Logic in Computer Science. Oxford University Press. pp. 1–168. ( ISBN 0-19-853762-X ). (para Matemáticos)
Schmidt, David A. Denotational Semantics: a methodology for language development. Allyn and Bacon, 1986. Disponível na página do autor.

Para revisão de Lógica

Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 2001. [ 511.3 ENDEma2 ]
Christopher C. Leary. A Friendly introduction to Mathematical Logic. Prentice Hall, 2000. ( ISBN: 0-13-010705-0 )
Shawn Hedman. A First Course in Logic: an introduction to model theory, proof theory, computability and complexity. Oxford, 2004. [ 160 HEDf ]
Huth, M.; Ryan, M. Logic in Computer Science: modelling and reasoning about systems. Cambridge, 2004 ( ISBN 978-0-521-54310-1 )
Srisvastava, S. M. A Course on Mathematical Logic. Springer, 2008. PDF na UFABC
Rautenberg, W. A Concise Introduction to Mathematical Logic. Springer, 2010. PDF na UFABC

Para revisão de Linguagens Formais

Sipser, M. Introdução à Teoria da Computação. Thomson Learning, 2007. [ 511.3 SIPi2 ]