**Course of Theoretical Computer Science (Informatica Teorica) 2011-2012.****
**

**Teacher:** Alberto
Pettorossi(Full Professor). Curriculum Vitae.**
**You can
talk to the teacher after the lectures or by appointment.

**6 cfu
(crediti formativi). Code: 8037394.**

**Settore
Scientifico Disciplinare: Sistemi di Elaborazione delle Informazioni. **

**ING-INF/05
09-H1 **

**60 hours
of face-to-face teaching (unique module).**

** **

**Contratto integrativo:
Proofs of Properties of Programs **

**(Dr. Ing. Valerio Senni,
research contract holder) (5 hours).**

**Lectures: from
03.10.11 to 04.02.12**

**Tuesday 11:30-13:15 (Room 01 n.e.)**

**Thursday 09:30-11:15 (Room 03 n.e.)**

**Exams and Seminars.**

**Same time and place as the
exams of the course: Automi e Linguaggi.
Please, visit that site.**

and no more than three exam calls per academic year.

with the solution of the take-home-exam.

of the project A1 (or the projects A1 and A2), ready for execution.

**Learning Objectives.** The course offers an
overview of the methods for the definition

of the semantics of the imperative, functional, logic, and concurrent
programming languages.

Those methods deepen the logical and algebraic understanding of various
techniques

for specifying and verifying properties of programs written in those languages.

Some programming projects and the use of suitable software tools will

reinforce the understanding of the theoretical notions.

**Detailed Syllabus and Exam Questions**.

**Take-home-exam: to be done by yourself.**

**Syllabus.**

**1.** Decidability and Turing
computability. Partial Recursive Functions.

**2. **Structural
induction, well-founded induction, and rule induction. Recursion Theorem.

**3. **Operational,
denotational, and axiomatic semantics of an imperative language.

Hoare's triples for partial correctness. Hoare's calculus:
soundness and relative completeness.

**4.**
Operational and denotational semantics of a first order functional language:

call-by-value and call-by-name regimes.

**5.**
Domain theory. A metalanguage for denotational semantics. Bekic's Theorem.

Inclusive predicates and proofs of properties of functional
programs.

**6.**
Operational and denotational semantics of a higher order functional language:
eager semantics

and lazy semantics. Fixpoint operators. Beta and eta rules.
Adequacy and full abstraction.

**7. **Operational
and denotational semantics of Horn-clause programs.

**8. **Dijkstra's
nondeterministic guarded commands. Owicki-Gries rules for parallel commands.

Milner's calculus for communicating concurrent processes.

**9.**
mu-calculus and proofs of communicating systems and protocols. Local model-checking.

**Requirements for the course: **Fundamentals notions of Computer Science. Algorithms and Data
Structures.

Elements of Algebra and
elements of Predicate Calculus.

**Attendance to
lectures is compulsory**.

**Previous
Exam Questions**

**Statistics of the outcome of previous exam
sessions.**

**Exam
Information:**

(i) Marks: 18 - 20: 10 exercises of the
take-home-exam + Project A1 + Written and Oral
Exam.

(ii) Marks: 21 - 25: 10 exercises of the
take-home-exam + Projects A1 and A2 + Written and Oral Exam.

(iii) Marks: 26 – 30L: all exercises of the take-home-exam + Projects A1
and A2 + Written and Oral Exam.

**Books:**

**Pettorossi,
A.: Semantics of Programming Languages**

Book for further reading:

-------------------------------------------------------------