Stockholm university logo, link to start page
Gå till denna sida på svenska webben

Type theory

The course provides an introduction to type theory with simple and dependent types, how it can be used to represent logical systems and proofs, and how proofs give rise to computable functions. The final part of the course covers applications of type theory.

Information for admitted students Spring 2023

Congratulations! You have been admitted at Stockholm University and we hope that you will enjoy your studies with us.

In order to ensure that your studies begin as smoothly as possible we have compiled a short checklist for the beginning of the semester.

Follow the instructions on whether you have to reply to your offer or not.
universityadmissions.se

 

Checklist for admitted students

  1. Activate your university account

    The first step in being able to register and gain access to all the university's IT services.

  2. Register at your department

    Registration can be done in different ways. Read the instructions from your department below.

  3. Read all the information on this page

    Here you will find what you need to know before your course or programme starts.

IMPORTANT

Your seat may be withdrawn if you do not register according to the instructions provided by your department.

Information from the department - courses

Here you can find information about online registration times, our learning platform, and what it means if you are conditionally admitted or placed on a reserve list.

First: Reply to your offer!

If you are offered a place or reserve place in the first notification of selection results, you must reply to it via Universityadmissions.se by 19 December to keep your place!

Info at Universityadmissions.se about replying to your offer

If you forget to do this, you must apply for the course again (assuming it is open for late application) if you want to take it.

Registration in Ladok

Once you are admitted to a course you must register online via student.ladok.se to keep your place. Online registration opens 3 January, and closes at different times for different courses.

For the following courses the last day for online registration is 9 January:

  • Mathematics I (only given in Swedish).
  • Courses in computer science or scientific computing given at KTH, so courses with course codes BE7008, BE7012, DA7054-61.

For other courses, the last day for online registration is 5 February if the course begins in the first half of the semester and 10 April if it begins in the second half.

Note that you cannot register online for degree project courses in mathematics, we will register you for these when your project plan has been approved.

Learning platform

Our course pages can be found at kurser.math.su.se.

On most of the course pages you can "self enrol", but doing this does not mean that you are registered for the course! In only gives you access to the course page. You always have to register in Ladok separately, see above about registration.

Conditionally admitted

It is quite common that a student at the time of application has not finished all courses that are given as special eligibility requirements for the course or programme the student has applied for. This will result in the admission status "Conditionally admitted".

We will go through the conditions just before course start. As long as the condition remains you cannot register for the course in Ladok. If the condition is still in place by course start, and you haven't received any notification about whether or not you'll be allowed to take the course or programme you have applied for, contact our student advisors. If the course is one where online registration closes early, contact us before it closes.

You can also be conditionally admitted because you need to pay a tuition fee. You can find more information on tuition fees here:

Payment and repayment of tuition fee

Placed on reserve list

If you have a reserve place for a course, we may be able to offer you a spot in which case we will contact you around the start of the semester. If you have a conditional reserve place and are offered a place on the course, you also need to fulfil the condition(s) before you can take your place on the course.

More information

New student: information about admission, registration, course literature and course web

During your studies: information about exams, our code of honour, student representation and IT resources

Contact for questions about studies

Welcome activities

Stockholm University organises a series of welcome activities that stretch over a few weeks at the beginning of each semester. The programme is voluntary (attendance is optional) and includes Arrival Service at the airport and an Orientation Day, see more details about these events below.
Your department may also organise activities for welcoming international students. More information will be provided by your specific department. 

su.se/welcomeactivities 


Find your way on campus

Stockholm University's main campus is in the Frescati area, north of the city centre. While most of our departments and offices are located here, there are also campus areas in other parts of the city.

Find your way on campus


Read more

New student

During your studies

Student unions


For new international students

Pre-departure information

New in Sweden

The following topics are covered:

Type theory: lambda calculus, contexts, forms of judgement, simple types, inductive types. Operational semantics: confluence and normalization. The Curry-Howard isomorphism. Martin-Löf type theory: dependent types, induction and elimination rules, identity types, universes. The Brouwer-Heyting-Kolmogorov interpretation of logic. Meaning explanations. Semantics of dependent types. Explicit substitution. Category theoretical models. One or more of the following areas of application of type theory are covered: homotopy theory, models for (constructive) set theory and proof assistants.