Semântica Formal (2014/1)

Carga horária: 60 hs (30 aulas de 1 hora e 40 minutos)
Créditos: 4
Horário: terças e quintas, 13:30 - 15:10 (turma A) e 15:30 - 17:10 (turma B)
Atendimento: Sala 220 do prédio 67

* Programa da disciplina

* Notas da P1 - turma A

* Notas da P1 - turma B

* **** RESULTADOS - turmas A e B *****

* Prova I

* Prova II

• Definições indutivas, indução estrutural e introdução a semântica operacional e sistema de tipos

• Linguagem L1, L2, L3

• Resumo de L3,

• Exceções e Subtipos

• Orientação a Objetos

• Semântica Axiomática (Respostas de Semântica Axiomática)

• Semântica Denotacional

Logic in Computer Science: Modelling and Reasoning about Systems
Michael Huth, Mark Ryan
Editora Cambridge University Press (ISBN 978852161610)

Types and programming languages
Pierce, Benjamin Pierce
Editora Mit Press (ISBN 0262162091)
Disponível em http://ieeexplore.ieee.org/xpl/bkabstractplus.jsp?bkn=6267321

Abaixo seguem ótimos artigos que tratam de assuntos que, de uma forma ou de outra, foram tratados nessa disciplina:

Retrospective: An Axiomatic Basis for Computer Programming - Entrevista com Tony Hoare

Technical Perspective: A Compiler's Story - Ótima introdução ao artigo Formal Verification of a Realistic Compiler (ver abaixo)

OCaml for the Masses

Solving the Unsolvable - Editorial da CACM sobre o artigo Proving Program Termination (ver abaixo)

Formal Verification of a Realistic Compiler

Proving Program Termination

Trabalho 2014-1

Turma A

Turma B