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

**How it works**: we meet on Fridays at 16:00 in the
meeting room 315 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.

**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 *pl[AT]software.imdea.org*.

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

Swivel:
Hardening WebAssembly against Spectre |
2021 | Shravan Narayan, Craig Disselkoen, Daniel Moghimi, Sunjay Cauligi, Evan Johnson, Zhao Gang, Anjo Vahldiek-Oberwagner, Ravi Sahita, Hovav Shacham, Dean Tullsen, Deian Stefan | Arpit |

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

08.07.2022 (Notes) | PACMAN:
Attacking ARM Pointer Authentication with Speculative Execution |
2022 | Joseph Ravichandran, Weon Taek Na, Jay Lang, Mengjia Yan | Arpit |

24.06.2022 (Notes) | Safe
Couplings: Coupled Refinement Types |
2022 | Lisa Vasilenko, Niki Vazou, Gilles Barthe | Lisa |

03.06.2022 (Notes) | Linearity
and Uniqueness: An Entente Cordiale |
2022 | Daniel Marshall, Michael Vollmer, Dominic Orchard | Sasha |

13.05.2022 | From
Fine- to Coarse-Grained Dynamic Information Flow Control and
Back |
2019 | Marco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, Deian Stefan | Marco |

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.