
Course unit
LOGICAL FOUNDATIONS OF FUNCTIONAL LANGUAGES
SC03119888, A.A. 2015/16
Information concerning the students who enrolled in A.Y. 2015/16
ECTS: details
Type 
ScientificDisciplinary Sector 
Credits allocated 
Educational activities in elective or integrative disciplines 
MAT/01 
Mathematical Logic 
6.0 
Course unit organization
Period 
Second semester 
Year 
1st Year 
Teaching method 
frontal 
Type of hours 
Credits 
Teaching hours 
Hours of Individual study 
Shifts 
Practice 
1.0 
8 
17.0 
No turn 
Lecture 
5.0 
40 
85.0 
No turn 
Examination board
Examination board not defined
Prerequisites:

Some basic knowledge in mathematical logic and set theory 
Target skills and knowledge:

The aim of this course is to provide a basic theoretical introduction to typed and nontyped functional programming. 
Examination methods:

Homeworks and oral exam. The student is required to discuss his solutions of some homeworks. 
Assessment criteria:

The exam will assess the knowledge acquired by the student on the topics of the course and his ability to use it on practical example. 
Course unit contents:

We first present the pure lambda calculus and show that all recursive functions are lambdarepresentable. Then we move to the simply typed lambda calculus, we study its relation with the implicative fragment of the intuitionistic propositional calculus and prove that it is strongly normalising by interpreting types into saturated subsets of lambda terms. To gain further expressivity other types are then introduced which have a direct interpretation in intuitionistic logic or in constructive set theory arriving in the end to polymorphic typed lambda calculus. For all the considered calculi we prove the main theorems of strong normalization and confluence and in some cases we also study the categorical semantics and its application to the categorical abstract machine. 
Planned learning activities and teaching methods:

Classroom lessons 
Additional notes about suggested reading:

Lecture notes 
Textbooks (and optional supplementary readings) 

J.Y.Girard, Y.Lafont, P.Taylor, Proofs and Types. : Cambridge University Press, .

H.Barendreght, The Lambda Calculus, its Syntax and Semantics. : NorthHolland, .

H.Barendreght,, Lambda Calculi with Types. : Oxford University Press, . Handbook of Logic in Computer Science


