Programming Languages & Security Reading Group at IMDEA

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]

Proposed Papers

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

Presented Papers

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:

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.

Guidelines for presenter

  1. 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.

  2. 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.

  3. 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, 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.