Lambda calculus, types and foundations of programming languages
Summary
Discover the theory behind modern functional programming languages through lambda calculus, a powerful model of computation that bridges mathematics, logic, and computer science.
About
In this course, you’ll explore both untyped and typed lambda calculi, including systems such as System T, System F, and PCF. You’ll learn how types shape computation, and how logical systems and programs connect through the Curry–Howard correspondence.
The course combines theory with practice, giving you the tools to design programs, analyse key properties like termination and confluence, and apply advanced proof techniques such as logical relations and realisability.
Ideal for students interested in the deep connections between programming, logic, and mathematical reasoning.
Prerequisites and selection
Entry requirements
For admission to the course successful completion of Logical theory (LOG111), or the equivalent, is
required.
English 6 or equivalent is also required.
Selection
Selection is based upon the number of credits from previous university studies, maximum 165 credits.
Facilities
The Faculty of Humanities is located in the Humanisten building at Renströmsgatan 6. The Department of Philosophy, Linguistics and Theory of Science has its premises on the 5th floor. Both the Faculty of Humanities and the adjacent Humanities Library offer several study areas and group rooms.
More information about facilities
Teaching is given in the form of lectures and individual assignments.
