Linguaggi di Programmazione: Semantica (2009/10, Laurea in Informatica)

Informazioni

Questa pagina conterrà eventuali note o materiale utilizzato nella mia parte del corso di Semantica.

Argomenti:

Il lambda-calcolo non tipato. Beta-eta riduzione. Semantica dinamica. Teorema di Church-Rosser. Forme normali e unicità. Strategia normalizzante leftmost-outermost.
- Rif: capitolo 7 del libro Mastroeni-Priami. Un'implementazione web. (provate singlestep, normal order = leftmost-outermost)
Gli encoding di Church: come rappresentare in lambda-calcolo non tipato booleani, naturali, coppie.
- Rif: vedi sotto.
La ricorsione nel lambda calcolo non tipato: il combinatore di punto fisso Θ
- Rif: Un'introduzione al lambda calcolo, Alcune note da un altro corso (capitolo 2, fino alla 2.7; appendice con la definizione dei vari combinatori)
Il lambda-calcolo tipato: semantica statica.
- Rif: capitolo 7 del libro Mastroeni-Priami; Winskel 11.1
Il lambda-calcolo tipato: semantica dinamica operazionale eager e lazy.
- Rif: Winskel 11.2, 11.6
Teoria dei domini.
- Rif: Winskel 5.4 (specialmente il Theorem 5.11), 8 (tranne 8.2,8.3.5)
Il lambda-calcolo tipato: semantica dinamica denotazionale lazy.
- Rif: Winskel 11.7

Libri:

I. Mastroeni, C. Priami. Semantica Operazionale: Strumenti e Applicazioni.
G. Winskel. The Formal Semantics of Programming Languages. (Disponibile anche in italiano)

Quesiti di alcuni esami precedenti: