
Course unit
TYPE THEORY
SCP6076357, A.A. 2019/20
Information concerning the students who enrolled in A.Y. 2019/20
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 
Lecture 
6.0 
48 
102.0 
No turn 
Prerequisites:

It is recommended to have followed an introductory course on logic but it is not strictly necessary. 
Target skills and knowledge:

The aim of this course is to provide a theoretical introduction to type theory in order to being able to appreciate its applications in computer science (functional program correctness possibly in computeraided way by means of a proofassistant) and in mathematics (development of constructive proofs possibly followed by their computeraided formalization and extraction of their computational contents). 
Examination methods:

Oral examination after completing some recommended exercises presented during the lectures. 
Assessment criteria:

The student is required to master the concepts presented in the course by himself/herself. The student is required to solve some easy exercises to test his understanding of the grasped concepts and its main properties. 
Course unit contents:

In the course the student will be introduced to the main typetheoretic concepts in order to being able to appreciate some key relevant applications of type theory in computer science, mathematics and even philosophy. He will be able to grasp the following aspects of the multifaceted nature of type theory:
1) The computational nature of type theory seen a typedlambda calculus a' la Church: type theory will be presented as a paradigm of a functional programming where to type programs with their specification in order to verify their correctness in computeraided way.
2) The settheoretic nature of type theory which makes it suitable to formalize proofs done in constructive mathematics and to extract their computational contents.
3)The predicative nature of dependent type theory a' la MartinLöf where types are defined in terms of an inductive generation process which extends recursive definitions. Examples of nonpredicative constructions will be described by employing the use of paradoxes.
4) The availability of intensional versions of type theory and extensional ones. These versions allows to get some decidable properties of typechecking useful to build a feasible and trustable proofassistant to formalize mathematical proofs expressed in an everyday mathematical language in a computeraided way.
The course will include a laboratory activity which will introduce the students to the use of a proofassistant (the French Coq or the Italian Matita or the Swedish Agda). 
Planned learning activities and teaching methods:

Lectures and laboratory activities. 
Additional notes about suggested reading:

Notes provided by the instructor. 
Textbooks (and optional supplementary readings) 

Bengt Nordström, Kent Petersson, Jan M. Smith, Programming in MartinLoef's Type Theory. : Oxford Uiniversity Press, 1990.

P. MartinLöf, Intuitionistic type theory. Notes by G. Sambin of a series of lectures given in Padua, June 1980. : Bibliopolis, 1984.

Innovative teaching methods: Teaching and learning strategies
 Laboratory
 Case study
 Interactive lecturing
 Working in group
 Questioning
 Action learning
 Problem solving
 Concept maps
 Loading of files and pages (web pages, Moodle, ...)
Sustainable Development Goals (SDGs)

