**UPDATE: meetings also take place in zoom5 with the password "plreading"**

**UPDATE2: we introduce guidelines for presenter after the format section**

**What it is**: the reading group is a bi-weekly meeting to discuss papers in PL and related areas.

**How it works**: we meet on Tuesdays at 14:30 in the meeting room 379 (or zoom5 with the password "plreading") to discuss the scheduled paper of the day. Each scheduled paper has a person in charge of leading the discussion, who is supposed to have read the paper. Other participants are highly encouraged to at least skim the paper, but it is optional, not mandatory.

**Who can participate**: anyone who is in the institute on the meeting day. Remote participation is also possible.

**How scheduling works**: to schedule a paper for the discussion, we choose one from the queue of proposed papers. To propose a paper send an email to Nikita. Before the next session we will vote whether to read the paper from the bottom of proposed papers table. Usually it is enough that three people, aside from the presenter, are willing to discuss the paper for it to be scheduled.

**What papers can be proposed**: any paper is fine, as long as it attracts enough interest from participants. We read more recent papers as happily as classic ones.

Paper | Year | Authors | Proposed by |
---|---|---|---|

Schizophrenia in contemporary mathematics |
1973 | Errett A. Bishop | Miëtek |

The Fire Triangle |
2020 | Pierre-Marie Pédrot, Nicolas Tabareau | Nikita |

The Taming of the Rew: A Type Theory with Computational Assumptions |
2021 | Jesper Cockx, Nicolas Tabareau, Théo Winterhalter | Nikita |

Date | Paper | Year | Authors | Presenter |
---|---|---|---|---|

13.07.2021 (Notes) | Bidirectional Type Checking for Relational Properties |
2019 | Ezgi Çiçek, Weihao Qu, Gilles Barthe, Marco Gaboardi, Deepak Garg | Lisa |

22.06.2021 (Notes) | Information, Processes and Games |
2016 | Samson Abramsky | Sasha |

08.06.2021 (Notes) | RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types |
2021 | Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg | Nikita |

23.03.2021 | Game Semantics: Easy as Pi |
2021 | Simon Castellan, Léo Stefanesco, Nobuko Yoshida | Sasha |

16.02.2021 | Functorial Semantics for Partial Theories |
2021 | Ivan di Liberti, Fosco Loregian, Chad Nester, Pawel Sobocinski | Franta |

02.02.2021 | Transfinite Step-Indexing for Termination |
2021 | Simon Spies, Neel Krishnaswami, Derek Dreyer | Nikita |

13.10.2020 | Dynamic Enforcement of Knowledge-based Security Policies |
2011 | Piotr Mardziel, Stephen Magill, Michael Hicks, Mudhakar Srivatsa | Panagiotis |

15.09.2020 | A Type-Theoretical Alternative to ISWIM, CUCH, OWHY |
1969 | Dana Scott | Nikita |

26.05.2020 | Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages |
2020 | Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser | Sasha |

12.05.2020 | Runners in action |
2019 | Danel Ahman, Andrej Bauer | Nikita |

11.02.2020 | Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq |
2020 | Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter | Franta |

17.12.2019 | Explicit Provability and Constructive Semantics |
2001 | Sergei N. Artemov | Miëtek |

03.12.2019 | Algebraic Operations and Generic Effects |
2003 | Gordon Plotkin, John Power | Alejandro |

19.11.2019 | Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible |
2018 | William J. Bowman, Youyou Cong, Nick Rioux, Amal Ahmed | Nikita |

05.11.2019 | The Syntax and Semantics of Quantitative Type Theory |
2018 | Robert Atkey | Alejandro |

29.10.2019 | Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus |
2019 | Andreas Abel, Christian Sattler | Franta |

15.10.2019 | Coherence of Type Class Resolution |
2019 | Gert-Jan Bottu, Ningning Xie, Koar Marntirosian, Tom Schrijvers | Niki |

01.10.2019 | Modular, Higher-Order Cardinality Analysis in Theory and Practice |
2014 | Ilya Sergey, Dimitrios Vytiniotis, Simon Peyton Jones | Panagiotis |

17.09.2019 | A Reasonably Exceptional Type Theory |
2019 | Pierre-Marie Pédrot, Nicolas Tabareau, Hans Jacob Fehrmann, Éric Tanter | Nikita |

23.07.2019 | Copatterns – Programming Infinite Structures by Observations |
2013 | Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer | Joakim |

16.07.2019 | Sequent Calculus as a Compiler Intermediate Language |
2016 | Paul Downen, Luke Maurer, Zena M. Ariola, Simon Peyton Jones | Panagiotis |

09.07.2019 | Polymorphism is not set-theoretic |
1984 | John Reynolds | Nikita |

11.06.2019 | Edit Lenses |
2012 | Martin Hofmann, Benjamin Pierce, Daniel Wagner | Jesus |

30.05.2019 | Type-and-Example-Directed Program Synthesis |
2015 | Peter-Michael Osera, Steve Zdancewic | Panagiotis |

14.05.2019 | Abstract I/O Specification |
2019 | Willem Penninckx, Amin Timany, Bart Jacobs | Ignacio |

05.04.2019 | Dijkstra Monads for All |
2019 | Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martinez, Cătălin Hriţcu, Exequiel Rivas, Éric Tanter | Nikita |

22.03.2019 | Implementing Modal Dependent Type Theory |
2019 | Daniel Gratzer, Jon Sterling, Lars Birkedal | Nikita |

08.03.2019 | Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus |
2018 | Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg | Niki |

14.02.2019 | Definitional Proof-Irrelevance without K |
2019 | Gaetan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau | Joakim |

Ideally, everyone attending a meeting should leave with good understanding of what the paper was about, even if they have not read it fully. Thus the presenters are expected to cover the following basic points:

- What is the problem that the paper is trying to solve?
- Why is that problem important?
- What is the main idea used to solve the problem?
- If the paper is old, what impact did it have?

We recommend to cover these points by first going through the paper structurally, briefly summarizing each section. Deeper technical discussion should follow the high level summary of whole paper.

Make sure that you can give the key ideas of the paper and present the big picture in the first 45-60 minutes of the session. Thus everyone should be able to understand the problem, the context, and the solution of the paper. You can mention what else it contains that you did not have time to properly cover.

Aim to extract and present the key ideas; omit non-crucial detail, keep high-level view. If the paper cannot be aptly summarized in 45-60 minutes, or is too technical, it may be not the best fit for the reading group.

In this summary discussion, moderate the questions from the participants. If a question goes into a deep detail, and does not directly address key ideas and intuitions, then suggest to return to this question after the high-level presentation.

Prepare a short summary of the paper and its sections. Mention the problem, its significance, key ideas of the approach, its limitations. You can also briefly mention the interesting contents of each section. Invite the participants to quietly read the summary in the beginning of the session.

For summary, you may use bullet-point style to extract key details, or use any other format you find suitable, as long as it gives an apt summary. For example, feel free to include typing rules, interesting figures, or any other relevant key material.

To prepare the summary, we suggest a collaborative online tool https://hackmd.io/, and will send you a link to a new shared sheet once your proposed paper is scheduled. We encourage you to use the summary to help guide the discussion. These notes will be kept for further reference on the webpage.