Admission requirements
There are no requirements.
Description
Computing systems become increasingly more complex and handle a variety of different tasks. As our society relies on these systems working correctly, we need formal descriptions of computational models and semantics of programming languages to be able to verify the correctness of computing systems. The computational models that we will study in this course range from the simplest functional model to probabilistic models that underpin statistical phenomena in optimisation and machine learning.
During the course, we will introduce several programming language, all coming with specific kinds of computational models that allow us to give semantics to these languages. This approach allows us to concretely understand the purpose of the corresponding computational model, while we can use the languages to write and run concrete programs. We will find that this variety of computational models and the resulting semantics have recurring patterns. Moreover, with increasing complexity of the models, we will need some framework that helps us organising our work. For that reason, we will also study bits of category theory, which will greatly ease our work with the various computational models. Category theory has become indispensable in the research of language semantics and many other areas of computer science. This means that this course will prepare you for working with modern tools of language theory and beyond.
The course will consist of lectures, complementary programming assignments, and a research project. Through the assignments, you will deepen your knowledge about the semantics, learn how they can lead directly to an implementation, and develop familiarity with the programming language Haskell. In the research project, you will study a complementary topic by reading the relevant literature, summarising the literature in an essay, and giving a short presentation.
Course objectives
At the end of the course, students are able to:
reason about various models of computation including functional, order-theoretic (complete lattices and domains), syntactic, and probabilistic models;
explain the relation between the operational and denotational semantics of programming languages;
formulate the semantics of imperative, functional, and probabilistic languages;
design correct-by-construction programs using type systems;
reason about computational models and semantics using concepts from category theory;
explain how properties of programs can be formally proven;
assess and communicate literature on the semantics of programming languages;
write programs involving recursive data types and side effects in Haskell.
Thus, this course will enable you to better understand and structure programs, to reason about the behaviour of computer systems, and to design your own programming language along with an associated semantics.
Timetable
In MyTimetable, you can find all course and programme schedules, allowing you to create your personal timetable. Activities for which you have enrolled via MyStudyMap will automatically appear in your timetable.
Additionally, you can easily link MyTimetable to a calendar app on your phone, and schedule changes will be automatically updated in your calendar. You can also choose to receive email notifications about schedule changes. You can enable notifications in Settings after logging in.
Questions? Watch the video, read the instructions, or contact the ISSC helpdesk.
Note: Joint Degree students from Leiden/Delft need to combine information from both the Leiden and Delft MyTimetables to see a complete schedule. This video explains how to do it.
Mode of instruction
The course will consist of lectures, programming assignments in pairs and a research project with a presentation session at the end.
Course load
Total hours of study: 168h
Lectures: 20h
Workgroups: 20h
Practicum: 60h
Self-study: 68h
Assessment method
The final grade is calculated as follows:
- Programming exercises: 40% (group grade)
- Written essay: 50% (individual)
- Presentation: 10% (individual)
In order to pass the course, each individual grade must be at least 5.5. Each component can be improved to obtain a passing grade by implementing the feedback that is provided.
Reading list
The main source is: Henning Basold, Two Voice Semantics.
Roberto Bruni and Ugo Montanari, Models of Computation. Springer, 2017.
Jan van Eijck and Christina Unger, Computational Semantics with Functional Programming. Cambridge University Press, 2010.
Glynn Winskel, The Formal Semantics of Programming Languages. MIT Press, 1994.
Registration
As a student, you are responsible for enrolling on time through MyStudyMap.
In this short video, you can see step-by-step how to enrol for courses in MyStudyMap.
Extensive information about the operation of MyStudyMap can be found here.
There are two enrolment periods per year:
Enrolment for the fall opens in July
Enrolment for the spring opens in December
See this page for more information about deadlines and enrolling for courses and exams.
Note:
It is mandatory to enrol for all activities of a course that you are going to follow.
Your enrolment is only complete when you submit your course planning in the ‘Ready for enrolment’ tab by clicking ‘Send’.
Not being enrolled for an exam/resit means that you are not allowed to participate in the exam/resit.
Contact
All information will be available on Brightspace and on the website.
Remarks
Software
Starting from the 2024/2025 academic year, the Faculty of Science will use the software distribution platform Academic Software. Through this platform, you can access the software needed for specific courses in your studies. For some software, your laptop must meet certain system requirements, which will be specified with the software. It is important to install the software before the start of the course. More information about the laptop requirements can be found on the student website.