First cycle
degree courses
Second cycle
degree courses
Single cycle
degree courses
School of Science
Course unit
SCP6076357, A.A. 2019/20

Information concerning the students who enrolled in A.Y. 2019/20

Information on the course unit
Degree course Second cycle degree in
SC1176, Degree course structure A.Y. 2014/15, A.Y. 2019/20
bring this page
with you
Number of ECTS credits allocated 6.0
Type of assessment Mark
Course unit English denomination TYPE THEORY
Website of the academic structure
Department of reference Department of Mathematics
Mandatory attendance No
Language of instruction Italian
Single Course unit The Course unit can be attended under the option Single Course unit attendance
Optional Course unit The Course unit can be chosen as Optional Course unit

Teacher in charge MARIA EMILIA MAIETTI MAT/01

ECTS: details
Type Scientific-Disciplinary 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 of
Individual study
Lecture 6.0 48 102.0 No turn

Start of activities 02/03/2020
End of activities 12/06/2020
Show course schedule 2019/20 Reg.2014 course timetable

Examination board
Board From To Members of the board
4 a.a. 2019/2020 01/10/2019 28/02/2021 MAIETTI MARIA EMILIA (Presidente)
BLECHSCHMIDT INGO (Membro Effettivo)
3 a.a. 2018/2019 01/10/2018 28/02/2020 MAIETTI MARIA EMILIA (Presidente)
CIRAULO FRANCESCO (Membro Effettivo)
SAMBIN GIOVANNI (Membro Effettivo)

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 computer-aided way by means of a proof-assistant) and in mathematics (development of constructive proofs possibly followed by their computer-aided 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 type-theoretic 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 typed-lambda 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 computer-aided way.

2) The set-theoretic 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 Martin-Löf where types are defined in terms of an inductive generation process which extends recursive definitions. Examples of non-predicative 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 type-checking useful to build a feasible and trustable proof-assistant to formalize mathematical proofs expressed in an every-day mathematical language in a computer-aided way.

The course will include a laboratory activity which will introduce the students to the use of a proof-assistant (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 Martin-Loef's Type Theory. --: Oxford Uiniversity Press, 1990.
  • P. Martin-Löf, Intuitionistic type theory. Notes by G. Sambin of a series of lectures given in Padua, June 1980. --: Bibliopolis, 1984. Cerca nel catalogo

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)
Good Health and Well-Being Affordable and Clean Energy Decent Work and Economic Growth