FIK3620 Types, Semantics, and Programming Languages 7.5 credits

Typer, semantik och programmeringsspråk

In this course, you will learn the fundamentals of programming language theory, including formal semantics, type systems, and type soundness proofs. The course contains both theory and practice. During the course, you will also implement an interpreter for a typed functional language, as well as solving various theoretical exercises.

Show course information based on the chosen semester and course offering:

Offering and execution

No offering selected

Select the semester and course offering above to get information from the correct course syllabus and course offering.

Course information

Content and learning outcomes

Course contents *

The course is divided into three separate modules, each covering different aspects on types, semantics, and programming language theory:
1. Operational semantics and the lambda calculus
   - Small-step and big-step operational semantics
   - Untyped lambda calculus
   - Fundamental typed functional programming
2. Typed lambda calculus with extensions
   - Type rules
   - Type soundness proofs
   - Semantics for let bindings, pairs, tuples, records, sums, and lists
   - References and exceptions
3. Subtyping and Polymorphism
   - Subtype polymorphism
   - Parametric polymorphism
   - Ad-hoc polymorphism
   - Structural and nominal type systems
   - Gradual typing

Intended learning outcomes *

After the course, the student will be able to
- Construct type soundness proofs
- Analyze type rules
- Analyze small-step and big-step operational semantics
- Implement an interpreter and a type checker for a typed functional language
- Apply untyped and simply typed lambda calculus with extensions

Course Disposition

No information inserted

Literature and preparations

Specific prerequisites *

No information inserted

Recommended prerequisites

Good knowledge in programming. Good basic knowledge in discrete mathematics and logic.
Knowledge in functional programming and compilers is beneficial, but is not a prerequisite.


No information inserted


No information inserted

Examination and completion

If the course is discontinued, students may request to be examined during the following two academic years.

Grading scale *

P, F

Examination *

  • EXA1 - Examination, 7.5 credits, Grading scale: P, F

Based on recommendation from KTH’s coordinator for disabilities, the examiner will decide how to adapt an examination for students with documented disability.

The examiner may apply another examination format when re-examining individual students.

See "Requirements for final grade" below.

Other requirements for final grade *

The student receives grade P if the following is fulfilled:
1. Active participation in seminars
2. Approved oral presentations at the seminars
3. Approved solutions to theoretical exercises
4. Approved submission and presentation of a software implementation
If the student cannot participate in a seminar, the student can do complementary work at another occasion.

Opportunity to complete the requirements via supplementary examination

No information inserted

Opportunity to raise an approved grade via renewed examination

No information inserted


David Broman

Ethical approach *

  • All members of a group are responsible for the group's work.
  • In any assessment, every student shall honestly disclose any help received and sources used.
  • In an oral assessment, every student shall be able to present and answer questions about the entire assignment and solution.

Further information

Course web

Further information about the course can be found on the Course web at the link below. Information on the Course web will later be moved to this site.

Course web FIK3620

Offered by

EECS/Software and Computer Systems

Main field of study *

No information inserted

Education cycle *

Third cycle

Add-on studies

No information inserted

Postgraduate course

Postgraduate courses at EECS/Software and Computer Systems