University of Warsaw - Central Authentication System

Logic and type theory

General data

Course ID:	1000-2M13LTT
Erasmus code / ISCED:	11.3 The subject classification code consists of three to five digits, where the first three represent the classification of the discipline according to the Discipline code list applicable to the Socrates/Erasmus program, the fourth (usually 0) - possible further specification of discipline information, the fifth - the degree of subject determined based on the year of study for which the subject is intended. / (0612) Database and network design and administration The ISCED (International Standard Classification of Education) code has been designed by UNESCO.
Course title:	Logic and type theory
Name in Polish:	Logika i teoria typów
Organizational unit:	Faculty of Mathematics, Informatics, and Mechanics
Course groups:	(in Polish) Grupa przedmiotów obieralnych dla informatyki magisterskiej- specjalność Języki programowania (in Polish) Przedmioty obieralne na studiach drugiego stopnia na kierunku bioinformatyka Elective courses for Computer Science and Machine Learning
Course homepage:	http://www.mimuw.edu.pl/~urzy/LTT
ECTS credit allocation (and other scores):	6.00 Basic information on ECTS credits allocation principles: the annual hourly workload of the student’s work required to achieve the expected learning outcomes for a given stage is 1500-1800h, corresponding to 60 ECTS; the student’s weekly hourly workload is 45 h; 1 ECTS point corresponds to 25-30 hours of student work needed to achieve the assumed learning outcomes; weekly student workload necessary to achieve the assumed learning outcomes allows to obtain 1.5 ECTS; work required to pass the course, which has been assigned 3 ECTS, constitutes 10% of the semester student load. view allocation of credits
Language:	English
Type of course:	elective monographs
Short description:	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.
Full description:	* 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.
Bibliography:	* Sorensen, M., Urzyczyn, P., Lectures on the Curry-Howard Isomorphism * Own material accessible in the web.
Learning outcomes:	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.
Assessment methods and assessment criteria:	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.

Classes in period "Winter semester 2024/25" (past)

Time span:	2024-10-01 - 2025-01-26	Selected timetable range: weekly course term Go to timetable MO TU W WYK TH FR CW
Type of class:	Classes, 30 hours more information Lecture, 30 hours more information
Coordinators:	Paweł Urzyczyn
Group instructors:	Paweł Urzyczyn, Daria Walukiewicz-Chrząszcz
Students list:	(inaccessible to you)
Credit:	Examination
Notes:	(in Polish) Wykład będzie odbywać się zdalnie, a ćwiczenia stacjonarnie.

Course descriptions are protected by copyright.
Copyright by University of Warsaw.