COURSES AND SEMINARS

SPEAKER: Damiano Mazza (CNRS)

The goal of automatic differentiation (AD) is to provide algorithms and techniques for efficiently computing the gradient of a function specified by a computer program. Developed since the 1970s and primarily used on limited sets of programs (typically, those expressing neural networks), AD recently reached the point where it applies to any
program whatsoever, as long as it computes a (possibly partial) function from tuples of real numbers to real numbers. This fully general evolution of AD has been dubbed "differentiable programming". This course will be an introduction to the theory of differentiable programming as is currently understood. Starting from the initial motivations, we will present the traditional AD techniques and see how they may be extended to more complex programs, up to a fully general functional language, and how the correctness of these extensions may be formally proved.

PREREQUISITES: Basic knowledge of the simply-typed lambda-calculus. Some background in semantics of programming languages will help but is not fundamental.

SPEAKER: Aleks Kissinger (University of Oxford)

Quantum circuits are a de facto "assembly language" for describing computations on a quantum computer. In this course, I'll briefly introduce the quantum circuit model and some of the basic ideas used in the construction of quantum algorithms based on this model. But mainly, we'll be cracking open quantum circuits -- and the quantum gates they are made out of -- to see what makes them tick. Along the way, we'll meet the ZX calculus, a graphical/algebraic "swiss army knife" of quantum computation, and show how the rewrite rules derived from the ZX calculus can be used to optimise quantum circuits and in some cases even efficiently simulate their behaviour without a quantum computer.

PREREQUISITES: Linear algebra with complex numbers. Some (very) basic graph theory, e.g. concepts of nodes, edges, paths, and connectedness.

SPEAKER: Prakash Panangaden (McGill University)

Probabilistic bisimulation, logical characterization, metrics: In this first lecture I will define Markov decision processes and labelled Markov processes on continuous state spaces, define probabilistic bisimulation a la Larsen and Skou, state the main logical characterization result and finally discuss pseudometrics whose kernel is probabilistic bisimulation. I will also present Kantrovich-Rubinstein duality and show how there are two equivalent ways of defining these metrics. Finally I will give the result of Ferns et al. on bounding differences in the optimal value functions in terms of the probabilistic bisimulation metric. In the second lecture I will define the MiCo distance which is a “cheap” substitute for the bisimulation metric and discuss its mathematical properties. I will start with the LK distance as a warm up. I will explain some basic aspects of representation learning and discuss our results on using the MiCo distance for representation learning. In the third lecture I will present the basic theory of reproducing kernel Hilbert spaces (RKHS) and show how the MiCo distance arises from an iteration in the space of kernels rather than in the space of metrics.

PREREQUISITES: Basic notions of metric spaces and topology, continuity, convergence, Banach’s fixed point theorem. Measure theory might be useful but not essential. Familiarity with nonprobabilistic bisimulation is expected.

SPEAKER: Christine Tasson

Probabilistic programming is a programming paradigm going beyond purely functional computation. It has been intensively developed in recent years, with the final purpose of encoding in the same settings various probabilistic models appearing in artificial intelligence and applied to statistical computing and machine learning. Numerous programming languages using higher-order functions and continuous probabilities have been developed. This universe is challenging from a semantical viewpoint and it is only recently that the meaning of these languages has been elucidated. A major obstacle had to be overcome to model continuous probabilities and functional programming languages (programs that can handle functions as arguments). In the first part of this tutorial, we will program first inference algorithms and use them to solve classical problems statistical learning. The second part will be dedicated to the semantics of probabilistic programming in the discrete settings. Finally, we will dive into semantics of programs with continuous probabilities.

PREREQUISITES: Lambda-Calculus, Typing Systems, Basic probability, Linear Logic

SPEAKER: Benjamin Kaminski (Saarland University)

Will my program terminate? If initially x == 2, will x be even after program termination? These are qualitative problems in program verification and answers to these questions are either yes or no, true or false. In order to make our life more difficult (but also much more interesting), we will study how to measure quantities instead of truth: How long will it take until my program terminates? Given the input value, what output value will my program produce? Given an observed output value, what was the input value? What can I still say if my program had access to randomness? In this course, we will investigate how to reason about such quantitative properties of software, i.e. typically infinite-state systems described symbolically by some programming language. To that end, we will first study qualitative deductive reasoning via Dijkstra's weakest [liberal] preconditions and strongest postconditions. We will then gradually lift qualitative to quantitative weakest pre / strongest post transformers. In particular, we will learn how to interpret weakest pre and strongest post meaningfully in a quantitative setting. We will also learn about a concept that Dijkstra missed to investigate (or did not care to investigate): strongest liberal post[conditions]. Finally, we will have a look at weakest pre transformers for probabilistic programs. We will learn how to use these transformers to reason about reachability probabilities and expected values. We will also learn how to adapt the probabilistic weakest pre calculus in order to reason about expected runtimes of probabilistic programs.

PREREQUISITES: Basics of FO logic and ideally also of Hoare logic. Basic knowledge of complete lattices is also beneficial.

SPEAKER: Marco Gaboardi (Boston University)

In this course we will study some of the formal tools that have been developed to formally support the correctness of software with respect to security and privacy requirements. We will focus on a few security and privacy properties such as: probabilistic non-interference and differential privacy. The basic formalism we will use is the one provided by relational program logics. Specifically, the class will introduce a probabilistic extension of relational program logics which supports reasoning about cryptographic security and differential privacy. We will see how different natural proofs for these properties can be expressed using this formalism.

SPEAKER: Niki Vazou (IMDEA)

Liquid Haskell is a refinement type checker developed to automatically, using an SMT solver, check simple program properties, for example safe-indexing and no division by zero. Over the years, Liquid Haskell was advanced to machine check more sophisticated properties, including security enforcement and non-interference.
In this course, we will start with an overview of Liquid Haskell and then we will use it to analyze the resources (represented as a tick monad) used by the Haskell functions. Time permitting, we will see how the same technology can be used to machine check more advanced properties, such as language metatheory.

SPEAKER: Valeria Vignudelli (CNRS)

In this seminar we will introduce equational theories allowing us to reason on probabilistic computational effects, modeled as monads. For instance, the theory of convex algebras characterizes the monad of probability distributions. Extensions of this theory include the combination of probabilistic and nondeterministic effects, which have led to the development of proof techniques for program equivalence. We will also present recent results on equational theories characterizing monads on metric spaces. These allow us to move from the notion of program equivalence to the notion of program distance.

SPEAKER: Delia Kesner (Université de Paris)

Quantitative techniques are emerging in different areas of computer science to face the challenges of resource aware computation. This seminar introduces "quantitative type systems", a formal tool that provides a clean theoretical understanding of the use of resources like execution time and space. We will discuss foundational issues covering (1) computational aspects, e.g. characterizing quantitative properties, establishing decidability results, defining new operational quantitative semantics, (2) semantical aspects, e.g. studying adequate sound and complete quantitative models.