Foundations of Computing (2010/2011)

Course code
Massimo Merro
Teaching is organised as follows:
Unit Credits Academic sector Period Academic staff
LOGICA 6 INF/01-INFORMATICS I semestre Damiano Macedonio
LINGUAGGI 6 INF/01-INFORMATICS I semestre Massimo Merro

Learning outcomes

Module: LOGICA
Introduction of the mathematical logic and its connection with other topics. Distinction between syntax and semantics. Formalization of properties in a formal language. Proof theory. Derivation and counter examples.

The aim of the course is to present the theoretical basis of programming languages. A number of paradigmatic untyped and typed languages will be introduced. The entire course will focus on the concepts of operational semantics and type system. Formal techniques for verifying the behaviour of programs will be introduced.


Module: LOGICA
Levels of reference. Language and meta-language.
Propositional and predicative logic(classic and intuitionistic).
Sequent calculus and definitional equations.
Systems LJ e LK. Cut elimination. Proof search.
Classical evaluation of formulae, both propositional and predicative.
Soundness, Completeness and Compactness for LK.
Decidability for predicative calculus.

(i) Mathematical induction over the natural numbers;
(ii) Structural induction;
(iii) Rule induction.
Operational semantics:
Big step and small step semantics for simple languages including
• Exp, Bool, languages for arithmetic and Boolean expressions
• the imperative language of while commands While
• the functional languages Fun and Lambda and simple variations on them; call-by-name and call-by-value semantics.
(i) Typing assignments for the languages Fun and Lambda
(ii) Progress and preservation.
(iii) For Lambda you should be familiar with the computational consequences of using types; in particular the need for explicit fixpoint operators.

Assessment methods and criteria

Module: LOGICA
Written and oral test.

The exam consists of a written and oral test.

Reference books
Author Title Publisher Year ISBN Note
Andrea Asperti, Agata Ciabattoni Logica a Informatica McGraw-Hill 2007
Carl A. Gunter Semantics of Programming Languages MIT Press 1992 0262570955
G. Winskel The formal Semantics of Programming Languages MIT Press 1993