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
Time and date on which the course is offered or a link to the website. The administration will complete this with the link to the website.
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
This has to be filled out by the key-user of the department.
Contact
All information will be available on Brightspace and on the website.
Remarks
None.