Semantics (2008/2009)

Course partially running

Course code
4S00065
Name of lecturer
Andrea Masini
Number of ECTS credits allocated
5
Academic sector
INF/01 - INFORMATICS
Language of instruction
Italian
Period
3° Q dal Apr 20, 2009 al Jun 19, 2009.

Lesson timetable

3° Q
Day Time Type Place Note
Thursday 3:30 PM - 5:30 PM lesson Lecture Hall F  
Friday 10:30 AM - 1:30 PM lesson Lecture Hall F  

Learning outcomes

The course introduces the main mathematical techniques developed in
the area of "formal semantics of programming languages":

* type systems
* operational semantics
* domain theory
* denotational semantics

Syllabus

1. operational semantics
1.1 definition of a simple imperative language
1.2 evaluation rules

2. induction
2.1 mathematical induction
2.2 structural induction
2.3 well founded induction

3. denotational semantics of a simple imperative language
3.1 a compositional semantics
3.2 the case of while-free programs
3.3 the treatment of the while

4. introduction to domain theory
4.1 complete partial orders
4.2 continuity
4.3 the Knaster-Tarski theorem
4.4 constructions on domains:
products of domains; function domains; flat domains

5 PCF
5.1 Terms and types
5.2 Free variables, bound variables and substitution
5.3 Typing
5.4 Evaluation (operational semantics)

6 Denotational Semantics of PCF
6.1 Denotation of types
6.2 Denotation of terms
6.3 Compositionality
6.4 Soundness

Assessment methods and criteria

--

Teaching aids

Documents