University: Technical University of Košice
Faculty: Faculty of Electrical Engineering and Informatics
Department: Department of Computers and Informatics
Course Number: 2616071 Course Name: Type theory
Type, scope and method of learning activities:
Course Type: Lecture, Numerical exercises
Recommended scope of the course content (in hours):
Full-time study (hours per week): 2,2
Part-time study (hours per semester): WT 26,26
Study Method:
Number of credits: 6
Recommended semester of study: WT
Recommended semester Study programme Study grade Study Method
1.rok WT Cybersecurity (KB_Ing_D_sk)
Informatics (INF_Ing_D_sk)
Computer Modelling (PM_Ing_D_sk)
Informatics (INF_Ing_D_en)
2.rok WT Cybersecurity (KB_Ing_D_sk)
Informatics (INF_Ing_D_sk)
Informatics (INF_Ing_D_en)
Level of study:
Course completion requirements:
Assessment and completion of the course: Credit test and examination
Continuous assessment: Student passes the continuous assessment and receives credits when he or she meets the requirement to obtain at least 16% out of 30%.
Final assessment: Student passes the final assessment and passes the examination when he or she meets the requirement to obtain at least 36% out of 70%.
Overall assessment: Overall assessment is the sum of the assessments obtained by students in the assessment period. The overall result is determined in accordance with the internal regulations of the Technical University in Košice. (Study Regulations, the internal regulation principles of doctoral studies)
Learning outcomes:
Students acquire basic knowledge about principles and methods of type theory starting with basic types across Church types, Curry types, polymorphic types up to dependent types. They understand different approaches to types and how to define the relations between them. They learn the approaches for defining several special types, e.g. recursive types and  existential types. Students understand the paradigm proposition-as-type based on Curry-Howard isomorphism. They practice particular approaches on examples in functional and procedural languages.
Brief course content:
1. Basic notions in type theory.
2. Untyped language of numbers and Booleans, NBL.
3. Untyped lambda calculus.
4. Typed NBL.
5. Simply typed lambda calculus.
6. Derived terms.
7. Product and sum types.
8. Recursion and recursive types.
9. Referential types.
10. Exceptions.
11. Subtypes.
12. Polymorphic types.
Recommended Reference Sources:
1. B.C.Pierce: Types and Programming Languages, MIT,2002
2. J.-Y. Girard: Proofs and types, Cambridge Univ.Press, 1989
3. J.R.Hindley: Basic simple type theory, Cambridge Univ.Press, 1997
4. R.Sethi: Programming Languages, WileyaSons, 1996
5. W.Horowitz: Higher-order Programming Languages, WileyaSons, 1982
Recommended optional program components:
Languages required for the course completion:
Course assessment:
Total number of students assessed: 1024
  A B C D E FX  
  38% 25% 19% 13% 2% 2%  
prof. RNDr. Valerie Novitzká, PhD.
doc. Ing. William Steingartner, PhD.
Ing. Ján Perháč, PhD.
Last modified: 31.08.2023
Approved by: person(s) responsible for the study program