Seminar in Theoretical CS, Winter Semester 2022/23

## News

- 26.10.2022: The student-topic-supervisor assignments are now available.
- 17.10.2022: The slides of the introductory presentation are now online.
- 02.06.2022: We are online!

## Introduction and Assignment of Topics

## Dates & Deadlines

20.10.2022 | Topic preferences due |

21.11.2022 | Detailed outline due |

22.12.2022 | Full report due |

13.01.2023 | Presentation slides due |

06.02./07.02.2023 | Seminar talks |

Note that the full versions of your report and your slides should be your *final submission* and the camera-ready versions should differ only with regard to *minor* remarks, comments, and corrections by your supervisor. Please feel free, however, to talk to your supervisor about submitting *preliminary versions before the due dates*.

## Overview

This seminar covers a variety of topics in the field of probabilistic programs. Roughly speaking, probabilistic programs are like ordinary programs, with an extra feature: the ability to make some sort of probabilistic choice. Here we show how one can exploit this feature to model, for instance, a duel between two cowboys. Describing randomized algorithms has been the classical application of these programs. Applications in biology, machine learning, quantum computing, security, and so on, have led to a rapidly growing interest in probabilistic programs in the last decade. For almost all programming languages, such as C, C#, Prolog, Haskell, Scala, LISP, a probabilistic variant does exist; and even a variant of Microsoft’s Excel has been developed – see the corresponding Wikipedia entry.

The topics considered in this seminar are mostly based on the book *Foundations of Probabilistic Programming* (edited by Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva and freely accessible). It contains 15 surveying chapters by different (teams of) authors, divided into five parts:

- Semantics,
- Verification.,
- Logic,
- Security, and
- Programming languages.

Additionally, we include some recent papers dealing with several different research areas in the field of probabilistic programs.

## Prerequisites

Basic knowledge in the following areas is expected:

- Probability theory
- Automata theory
- Mathematical logic

## Topics

**(Move the cursor over the entry to see the corresponding abstract.)**

Chapters of *Foundations of Probabilistic Programming*:

- [Semantics] (Ch.1) Fredrik Dahlqvist, Dexter Kozen, Alexandra Silva:
*Semantics of Probabilistic Programming: A Gentle Introduction*(44 pages) (B)- Student: (1) Bashar Hamdan, (2) Dinis Vitorino
- Supervisor: (1) Ira Fesefeldt, (2) Jip Spel

- [Semantics] (Ch.2) Sam Staton:
*Probabilistic Programs as Measures*(35 pages) (M)- Student: Maximilian Vöcklinghaus
- Supervisor: Philipp Schroer

- [Semantics] (Ch.4) Ugo Dal Lago:
*On Probabilistic Lambda-Calculi*(27 pages) (M)- Student: Juan Stücker
- Supervisor: Tobias Winkler

- [Verification] (Ch.5) Gilles Barthe, Justin Hsu:
*Probabilistic Couplings from Program Logics*(43 pages) (M)- Student: Zihan Zhou
- Supervisor: Raphaël Berthon

- [Verification] (Ch.6) Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja:
*Expected Runtime Analysis by Program Verification*(39 pages) (B)- Student: Bayza Akyüz
- Supervisor: Bahare Salmani

- [Verification] (Ch.7) Krishnendu Chatterjee, Hongfei Fu, Petr Novotný:
*Termination Analysis of Probabilistic Programs with Martingales*(41 pages) (M)- Student: Lasse van der Woude
- Supervisor: Joost-Pieter Katoen

- [Verification] (Ch.8) Sriram Sankaranarayanan:
*Quantitative Analysis of Programs with Probabilities and Concentration of Measure Inequalities*(40 pages) (M)- Student: –
- Supervisor: –

- [Programming languages] (Ch.13) Lampropoulos Leonidas, Benjamin C. Pierce, Li-yao Xia, Diane Gallois-Wong, Catalin Hritcu, John Hughes:
*Luck: A Probabilistic Language for Testing*(44 pages) (B)- Student: Mohamed Ali Chelbi
- Supervisor: Philipp Schroer

- [Programming languages] (Ch.14) Andrew D. Gordon, Claudio Russo, Marcin Szymczak, Johannes Borgström, Nicolas Rolland, Thore Graepel, Daniel Tarlow:
*Tabular: Probabilistic Inference from the Spreadsheet*(47 pages) (B)- Student: Ming Cheng Lee
- Supervisor: Alexander Bork

- [Programming languages] (Ch.15) Michael Carbin, Sasa Misailovic:
*Programming Unreliable Hardware*(39 pages) (B)- Student: Sven Farwig
- Supervisor: Alexander Bork

**Additional Papers**

- Zixin Huang, Saikat Dutta, Sasa Misailovic:
*Automated quantized inference for probabilistic programs with AQUA*. Innov. Syst. Softw. Eng. 18(3): 369-384 (2022) (M)- Student: Hanbin Chen

- Supervisor: Bahare Salmani

- Gilles Barthe, Charlie Jacomme, Steve Kremer:
*Universal Equivalence and Majority of Probabilistic Programs over Finite Fields*. ACM Trans. Comput. Log. 23(1): 5:1-5:42 (2022) (M)- Student: –

- Supervisor: –

- Marcelo Navarro, Federico Olmedo:
*Slicing of Probabilistic Programs Based on Specifications (Extended Abstract)*. ECOOP 2022: 34:1-34:2 (B)- Student: Christopher Zeise

- Supervisor: Alexander Bork

- Alessandro Abate, Mirco Giacobbe, Diptarko Roy:
*Learning Probabilistic Termination Proofs*. CAV (2) 2021: 3-26 (B)- Student: Nils Sommerfeld

- Supervisor: Bahare Salmani

- Jialu Bao, Marco Gaboardi, Justin Hsu, Joseph Tassarotti:
*A separation logic for negative dependence*. Proc. ACM Program. Lang. 6(POPL): 1-29 (2022) (M)- Student: –

- Supervisor: –

- Di Wang, Jan Hoffmann, Thomas W. Reps:
*A Denotational Semantics for Low-Level Probabilistic Programs with Nondeterminism*. MFPS 2019: 303-324 (B/M)- Student: –

- Supervisor: –

- Daniel J. Fremont, Edward Kim, Tommaso Dreossi, Shromona Ghosh, Xiangyu Yue, Alberto L. Sangiovanni-Vincentelli & Sanjit A. Seshia:
*Scenic: A language for scenario specification and data generation*. Machine Learning (2022)(B)- Student: (1) Farid Qasimov, (2) Luca Kempkes

- Supervisor: (1),(2) Tim Quatmann

- Timon Gehr, Samuel Steffen, Martin T. Vechev:
*λPSI: exact inference for higher-order probabilistic programs*. PLDI 2020: 883-897 (B)- Student: Rika Kade

- Supervisor: Lutz Klinkenberg

- Raven Beutner, C.-H. Luke Ong, and Fabian Zaiser:
*Guaranteed bounds for posterior inference in universal probabilistic programming*. PLDI 2022: 536–551 (M)- Student: –
- Supervisor: –

## Registration

Registration to the seminar is handled via the SuPra system.

## Grading Scheme

You can access the grading scheme here: https://moves.rwth-aachen.de/wp-content/uploads/seminar_grading_scheme.pdf

## Additional Material

- Report template
- Presentation template
- How to Write a Seminar Paper
- Ethische Richtlinien für das Verfassen wissenschaftlicher Arbeiten
- How to Give Presentations
- Introduction to LaTeX