Logic and type theory

elective monographs

This course will cover an introduction to various typed systems and their logical interpretations in the spirit of the "formulas as types" paradigm, also known as Curry-Howard isomorphism. In particular we will consider intuitionistic logic, linear logic and type-theoretical foundations for computer-assisted reasoning.

* Basic lambda-calculus recalled.

* Introduction to intuitionistic logic.

* Curry-Howard isomorphism.

* Logic as a dialogue game.

* Introduction to linear logic.

* Classical logic and non-local control.

* Polymorphism.

* Dependent types.

* The Calculus of Constructions and its generalizations (PTS).

* System Coq

* Inductive and recursive types.

* Introduction to homotopy type theory.

* Sorensen, M., Urzyczyn, P., Lectures on the Curry-Howard Isomorphism

* Own material accessible in the web.

Knowledge:

+ Knows the basics of intuitionistic and linear logic;

+ Knows the computational interpretations of various logics, including classical logic;

+ Can distinguish between proof-theoretic paradigms;

+ Knows the expressive power of various typed systems and knows

the corresponding logics;

+ Knows the basics of system Coq;

Skills:

+ Can interpret logical constructions as computational tasks;

+ Can write a simple proof in Coq;

Competences:

+ Understands the relations between computational and logical phenomena;

+ Is prepared to independentently typed systems and computer-assisted reasoning.

To pass the subject, you must pass the exercises and pass the exam (written, stationary).

The final grade will be determined on the basis of the exam.

To pass the exercises, it is necessary to submit homework.

It is the teacher who decides about passing the exercises.

Those who have completed their homework assignments and declared their readiness for the exam no later than January 8, 2023 can take the zero exam.

In the case of completing the course by a doctoral student, the student will read a selected recent research article and a chat with a lecturer about the article will be a part of the exam.