Logic and type theory 1000-2M13LTT

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 7, 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.

* Sorensen, M., Urzyczyn, P., Lectures on the Curry-Howard Isomorphism
* Own material accessible in the web.

Information on level of this course, year of study and semester when the course unit is delivered, types and amount of class hours - can be found in course structure diagrams of apropriate study programmes. This course is related to the following study programmes:

• Bachelor's degree, first cycle programme, Computer Science
• Master's degree, second cycle programme, Computer Science

Additional information (registration calendar, class conductors, localization and schedules of classes), might be available in the USOSweb system:

• Description of 1000-2M13LTT in USOSweb