Remote participation (Zoom): https://uu-se.zoom.us/j/64840179614

The course aims to make PhD students familiar with some of the core programming language techniques and approaches. After this course, students will be able to read and follow current research papers in the covered areas. Additionally, students will practice reading and reviewing papers, and preparing and giving presentations.

Prerequisites

basic logic
a basic compiler course is recommended
a basic understanding of structural operational semantics will be helpful

Course Schedule

Below is the tentative schedule for the course; changes may still occur. The lecture time is 13:00-16:00. Note that the starting time is 13 sharp! Typically, the lecture of topic LaTeX: n+1 will coincide with the seminar related to topic .

Date	Location	Topic
Thursday 31/3	105150	Introduction, History of Programming Languages
Monday 11/4	105130 (NB!)	Seminar (History) Formal Semantics
Monday 25/4	105150	Seminar (Semantics) Dataflow Analysis
Monday 2/5	105150	Seminar (Dataflow)
Monday 9/5	103150 (NB!)	Empirical Evaluation
Monday 16/5	105150	Seminar (Evaluation) Program Synthesis
Monday 30/5	105130 (NB!)	Seminar (Synthesis) Separation Logic
Monday 13/6	105150	Closing Seminar (Separation Logic) Guest lecture by Johannes Borgström (Probabilistic Programming)

The hope is to run the course as an in-person event, but online participation will be offered when needed or when the general situation necessitates.

Course Structure

The course will consist of lectures by the teachers Tobias Wrigstad, Elias Castegren and Eva Darulova that will provide an introduction to each topic and seminars for consolidating and discussing the introduced material. In preparation for the seminars, students will read and review research papers and write summaries.

Tentative Topics

History of Programming Languages: Since the invention of programming languages, and the popularisation of compilers, there have been thousands of programming languages designed and used, and thousands designed but not used. Sometimes, the success of a programming language is accidental; sometimes it is the result of a well-oiled marketing machine; sometimes popularisation comes from riding on a particular fad. Sometimes, the success of a programming language can be "measured", not by its uptake by developers, but by its influences on other languages. In this part of the course, we will look at the historical development of programming languages, and look closer at some interesting and influential programming languages, and trace some features through the ages.

Type systems: Most programmers are familiar with some notion of types. Whether working in a statically or a dynamically typed language, types describe the shape of data, how it should be interpreted, and which operations are available on it. For statically typed languages, type systems provide a light weight static analysis that rules out obviously incorrect behaviours, such as interpreting a string as an integer. Recently, type systems have also been used to guarantee more sophisticated properties, for example the safe low-level memory management and parallelism of Rust. In this part of the course we will look at how type systems are formally defined, how we can reason about their soundness, and how the specification of a type system differs from the implementation we would find in the type checker of a compiler.

Dataflow Analysis: Dataflow analysis allows to prove the absence of certain types of bugs in a program fully automatically, and is also the basis for many compiler optimizations. The analysis computes all the possible values that a variable may or must have, which can for instance prove the absence of array-of-out-bounds errors or enable dead code elimination. In this part of the course, we will cover the basic theory underlying dataflow analysis, some of the classic analyses and discuss limitations and tradeoffs.

Program logics: Best practices for software engineering prescribe using testing to find bugs and avoid regression as software evolves. But tests can only ever prove the presence of bugs, not their absence. Proving that a program is correct with respect to some specification is a much larger endeavour, especially in the presence of pointers and mutable state. In this part of the course we will look at how to formally reason about a program's behaviour using pre- and post-conditions and Hoare logic, touching upon separation logic which can be used to reason about data-structures with pointers.

Probabilistic Programming: A probabilistic program does not solve a task in the way that a 'normal' computer program does by running and computing a result or performing an action. Rather, a probabilistic program defines as a statistical model that one can analyze with a variety of (automated) tools. These tools in turn build on many 'standard' programming languages ideas and techniques to automate the process of statistical inference. In this part of the course, we will introduce the core concepts and primitives that most probabilistic programming languages support, look at some of the basic inference algorithms and explore how programming language ideas such as static analysis, synthesis and slicing can be adapted and applied in this domain.

Empirical Studies: Sometimes, evaluating a particular type system, program logic, or program analysis is possible by comparing their expressivity, their ability to establish certain invariants, or avoid false positives or false negatives. Often, it is necessary to go beyond purely theoretical comparisons, and undertake empiric studies. For example, how common are the errors excluded by our new analysis, in relation to the behaviours that confuse us enough to report false positives? If we study large code repositories to answer that question -- how do we handle the fact that such collections of code typically contain large numbers of copies of the same code? How does one go about concluding that a particular compiler optimisation is a true optimisation, when the behaviours of typical benchmarks can introduce enough jitter in a system that introduces timing variations across different runs? How to deal with JIT-compilation and garbage collection? In this part of the course we will look at some examples of how different empirical methodologies have been used to answer different research questions.