Reading Group

In the weekly reading group session we discuss a paper from the literature on programming languages. Currently reading group sessions are on Wednesdays at 11:00.

The reading group is organized as follows:

  • All participants read the paper in advance.
  • The moderator short presentation (5/10 minutes) during which they summarize the selected reading material. The presentation should focus more on motivation/contributions and less on technical details, but if the moderator feels like giving a longer presentation in which they do more explanation then that’s fine.
  • The moderator may also prepare a few questions or discussion points for the participants.
  • The remainder of the meeting is dedicated to discussing the paper.
  • At the end of the session a moderator is selected for the next session, who will propose reading material before the weekend.

The moderator can suggest whatever they want from any source (paper, blog posts, keynote, e-mail thread, forum post, etc…), but should keep the following guidelines in mind:

  1. The material should be PL related.
  2. The material can reasonably be consumed in at most 2 hours by the average PL group member. For longer papers, consider restricting to a specific section(s).

New entries should be added to _data/reading-group.yml.

Past Sessions

Wed, Jun 19, 2024 at 11:00 in Turing 0.E420
Socio-Technical Grounded Theory for Software Engineering

By Rashina Hoda in IEEE Transactions on Software Engineering

Moderator: Sára Juhošová

The paper is quite long, but sections 1, 2, 3, 4.1, and 5 are the most important. Alternatively, you can also watch this short talk done by the author https://youtu.be/K4NID7M8X1Y

Wed, Jun 12, 2024 at 11:00 in Turing 0.E420
Dependent Ghosts Have a Reflection for Free

By Théo Winterhalter

Moderator: Lucas Escot

Wed, May 01, 2024 at 11:00 in Turing 0.E420
Correct and Complete Type Checking and Certified Erasure for Coq, in Coq

By Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, Théo Winterhalter

Moderator: Jesper Cockx

Since it's a very long paper, we will focus on the following sections 1 (Introduction), 2.1 (Definition of the Syntax and Environments), 2.5 (Definition of Typing), 3.2 (Conversion Algorithmic presentation with equality and reduction), 5.1 (Technical Insight), 8 (Conclusion and Future Work)

Wed, Mar 20, 2024 at 11:00 in Turing 0.E420
Beyond Polarity: Towards A Multi-Discipline Intermediate Language with Sharing

By Paul Downen and Zena M. Ariola

Moderator: Jaro Reinders

Please read section 1 and 2.

Wed, Mar 06, 2024 at 11:00 in Turing 0.E420
Definitional Functoriality for Dependent (Sub)Types

By Théo Laurent, Meven Lennon-Bertrand, Kenji Maillard

Moderator: Jesper Cockx

I will only prepare a minimal introduction and hope to have an interactive discussion afterwards. I propose we focus our attention on sections 1-3.

Wed, Feb 28, 2024 at 11:00 in Turing 0.E420
How statically-typed functional programmers write code

By Justin Lubin and Sarah E. Chasins

Moderator: Sára Juhošová

I'd like to make the session somewhat more interactive, so you don't per se have to read the paper, but please do bring your laptop!

Wed, Feb 21, 2024 at 11:00 in Turing 0.E420
Live Pattern Matching with Typed Holes

By Yongwei Yuan, Scott Guest, Eric Griffis, Hannah Potter, David Moon and Cyrus Omar

Moderator: Aron Zwaan

Now with hot-press video upload https://www.youtube.com/watch?v=n67NgeQ-c20

Wed, Feb 14, 2024 at 11:00 in Turing 0.E420
Definite Clause Grammars for Language Analysis

By Fernando C. N. Pereira and David H. D. Warren in Artificial Intelligence

Moderator: Peter Mosses

I will give an introduction to Definite Clause Grammars, which appear to be closely related to the data-dependent grammars supported by Iguana. For reading, I propose §3 (13 pages) of a seminal article about DCGs.

Wed, Jan 24, 2024 at 11:00 in Turing 0.E420
Builtin Types viewed as Inductive Families

By Guillaume Allais

Moderator: Lucas Escot

Wed, Jan 17, 2024 at 11:00 in Turing 0.E420
Synthesizing Abstract Transformers

By Pankaj Kumar Kalita, Sujit Kumar Muduli, Loris D'Antoni, Thomas Reps and Subhajit Roy

Moderator: Dennis Sprokholt

Wed, Jan 17, 2024 at 12:00 in Turing 0.E420
ITrees

By Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce and Steve Zdancewic

Moderator: Casper Bach Poulsen

Wed, Jan 17, 2024 at 11:00 in Turing 0.E420
Reasoning about Effect Interaction by Fusion

By Zhixuan Yang and Nicolas Wu

Moderator: Casper Bach Poulsen

Wed, Jan 17, 2024 at 11:00 in Turing 0.E420
Shape Analysis

By Reinhard Wilhelm, Mooly Sagiv and Thomas Reps

Moderator: Soham Chakraborty

Wed, Nov 22, 2023 at 11:00 in Turing 0.E420
Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference

By Ishan Bhanuka, Lionel Parreux, David Binder, and Jonathan Immanuel Brachthäuser

Moderator: Aron Zwaan

Wed, Nov 08, 2023 at 11:00 in Turing 0.E420
Effects for Less

By Alexis King in ZuriHac 2020

Moderator: Jaro Reinders

Wed, Sep 27, 2023 at 11:00 in Turing 0.E420
Tabled Typeclass Resolution

By Daniel Selsam, Sebastian Ullrich, Leonardo de Moura in arxiv

Moderator: Bohdan Liesnikov

Wed, Sep 20, 2023 at 11:00 in Turing 0.E420
Automating Program Transformation with Coccinelle

By Julia Lawall and Gilles Muller in NFM 2022

Moderator: Layne Liu

Wed, Sep 06, 2023 at 11:00 in Turing 0.E420
One Parser to Rule Them All

By Ali Afroozeh and Anastasia Izmaylova in Onward! 2015

Moderator: Jaro Reinders

Wed, Jul 12, 2023 at 11:00 in Turing 0.E420
Backpack: Retrofitting Haskell with Interfaces

By Scott Kilpatrick, Derek Dreyer, Simon Peyton Jones and Simon Marlow in POPL14

Moderator: Cas van der Rest

Wed, Jul 05, 2023 at 11:00 in Turing 0.E420
Deriving a Lazy Abstract Machine

By Peter Sestoft in Journal of Functional Programming

Moderator: Jesper Cockx

If you're in a hurry, read the first three sections and skip the proofs

Wed, Apr 26, 2023 at 10:45 in Turing 0.E420
Calculating Compilers Categorically

By Conal Elliott in Unpublished draft

Moderator: Cas van der Rest

Wed, Apr 19, 2023 at 11:00 in Turing 0.E420
Classical lambda calculus in modern dress

By J. M. E. Hyland in Mathematical Structures in Computer Science

Moderator: Arnoud van der Leer

2.1, 2.2, 3.1 and the main theorem, 4.11

Wed, Mar 15, 2023 at 11:00 in Turing 0.E420
Functional Pearl: Heterogeneous random-access lists

By Wouter Swierstra in Journal of Functional Programming

Moderator: Lucas Escot / Jesper Cockx

Wed, Mar 08, 2023 at 11:00 in Turing 0.E420
MLIR: scaling compiler infrastructure for domain specific computation

By Chris Lattner, Mehdi Amini, Uday Bondhugula, Albert Cohen, Andy Davis, Jacques Pienaar, River Riddle, Tatiana Shpeisman, Nicolas Vasilache, Oleksandr Zinenko in ACM

Moderator: Jaro Reinders

Wed, Mar 01, 2023 at 11:00 in Turing 0.E420
Register Allocation: What Does the NP-Completeness Proof of Chaitin et al. Really Prove? Or Revisiting Register Allocation: Why and How

By Florent Bouchez, Alain Darte, Christophe Guillon, Fabrice Rastello

Moderator: Dennis Sprokholt

Wed, Feb 22, 2023 at 11:00 in Turing 0.E420
A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs

By Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna

Moderator: Cas van der Rest

Wed, Feb 15, 2023 at 11:00 in Turing 0.E420
Coq à la carte: a practical approach to modular syntax with binders

By Yannick Forster, Kathrin Stark

Moderator: Bohdan Liesnikov

Wed, Feb 08, 2023 at 11:00 in Turing 0.E420
Program Testing and the Meaning Explanations of Intuitionistic Type Theory

By Peter Dybjer in Martin-Löf festschrift

Moderator: Jesper Cockx

You can skip section 1.3

Wed, Feb 01, 2023 at 11:00 in Turing 0.E420
Evaluating Linear Functions to Symmetric Monoidal Categories

By Jean-Philippe Bernardy, Arnaud Spiwack

Moderator: Lucas Escot

Reading up to (and including) section 4 would be good.

Wed, Jan 25, 2023 at 11:00 in Turing 0.E420
A principled approach to REPL interpreters

By Thomas van Binsbergen, Mauricio Verano Merino, Pierre Jeanjean, Tijs van der Storm, Benoit Combemale, Olivier Barais in Onward! 2020

Moderator: Jeff Smits

Wed, Dec 14, 2022 at 11:00 in Turing 0.E420
The Verse Calculus : a Core Calculus for Functional Logic Programming

By Lennart Augustsson, Joachim Breitner, Koen Claessen, Ranjit Jhala, Simon Peyton Jones, Olin Shivers, Tim Sweeney in HaskellX

Moderator: Bohdan Liesnikov

Sections 1, 2 and then either 3 or 4 and 5, depending on your preference

Wed, Dec 07, 2022 at 11:00 in Turing 0.E420
Data-Codata Symmetry and its Interaction with Evaluation Order

By David Binder, Julian Jabs, Ingo Skupin, Klaus Ostermann

Moderator: Jaro Reinders

Wed, Nov 09, 2022 at 11:00 in Turing 0.E420
Supercompilation by Evaluation

By Maximilian Bolingbroke, Simon Peyton Jones

Moderator: Dennis Sprokholt

Wed, Oct 26, 2022 at 11:00 in Turing 0.E420
Controlling Unfolding in Type Theory

By Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, Lars Birkedal

Moderator: Jesper Cockx

Wed, Oct 12, 2022 at 11:00 in Turing 0.E420
Constraint-Based Refactoring

By Friedrich Steimann

Moderator: Daniel Pelsmaeker

Wed, Oct 05, 2022 at 11:00 in Turing 0.E420
A Tutorial on Graph Transformation

By Barbara König, Dennis Nolte, Julia Padberg, and Arend Rensink

Moderator: Luka Miljak

Wed, Sep 28, 2022 at 11:00 in Turing 0.E420
Future Directions for Optimizing Compilers

By Nuno P. Lopes, John Regehr

Moderator: Dennis Sprokholt

Wed, Sep 14, 2022 at 11:00 in Turing 0.E420
Specification, Implementation and Verification of Refactorings

By Max Schäfer

Moderator: Daniel Pelsmaeker

Chapter 2 Sections 2.3 and 2.4 on access construction and locked names

Wed, Sep 07, 2022 at 11:00 in Turing 0.E420
TypOS: An Operating System for Typechecking Actors

By Guillaume Allais, Malin Altenmüller, Conor McBride, Georgi Nakov, Fredrik Nordvall Forsberg, and Craig Roy

Moderator: Jesper Cockx

Talk recording at https://youtu.be/2ZmoexvTw6c?t=118, slides at https://fredriknf.com/talks/TYPES_2022/typOS.pdf, user manual at https://github.com/msp-strath/TypOS

Wed, Jul 13, 2022 at 11:00 in Turing 0.E420 / Jesper's Zoom Room
Histogram: You have to know the past to understand the present

By Tomas Petricek

Moderator: Alex Chichigin

Wed, Jun 29, 2022 at 11:00 in Turing 0.E420 / Jesper's Zoom Room
Keynote: How to specify it! (...)

By John Hughes in YouTube

Moderator: Jesper Cockx

Wed, Jun 22, 2022 at 11:00 in Turing 0.E420 / Luka's Zoom Room
Large-scale semi-automated migration of legacy C/C++ test code

By Mathijs T. W. Schuts, Rodin T. A. Aarssen, Paul M. Tielemans, Jurgen J. Vinju

Moderator: Luka Miljak

Wed, Jun 08, 2022 at 11:00 in Turing 0.E420 / Casper's Zoom Room
Monad transformers and modular interpreters

Moderator: Casper Bach Poulsen van der Rest

Also https://www.typetheoryforall.com/2022/05/09/17-The-Lost-Elegance-of-Computation-(Conal-Elliott).html

Wed, May 25, 2022 at 11:00 in Turing 0.E420 / Cas' Zoom Room
Monad transformers and modular interpreters

By Sheng Liang, Paul Hudak, Mark Jones in ACM

Moderator: Cas van der Rest

Wed, Mar 23, 2022 at 11:00 in Alex' Zoom Room
Effective Extensible Programming: Unleashing Julia on GPUs

By Tim Besard, Christophe Foket, Bjorn De Sutter

Moderator: Alex Chichigin

Wed, Mar 09, 2022 at 11:00 in Jeff's Zoom Room
Abstracting gradual typing

By Ronald Garcia, Alison M. Clark, Éric Tanter in ACM

Moderator: Jeff Smits

Sections 1-4 (section 4 is the meat of the paper). If you have time left => skim section 5 and go to section 6.

Wed, Mar 02, 2022 at 11:00 in Aron's Zoom Room
Elaborating dependent (co)pattern matching: No pattern left behind

By Jesper Cockx, Andreas Abel

Moderator: Aron Zwaan

Sections 2 and 4.1 - 4.3, referring back to section 3 when required

Wed, Feb 09, 2022 at 11:00 in Jaro's Zoom Room
Interaction nets

By Yves Lafont in ACM

Moderator: Jaro Reinders

Wed, Feb 02, 2022 at 11:00 in Arjen's Zoom Room
HVM; How!?

By Kindelia in Github

Moderator: Arjen Rouvoet

Wed, Jan 26, 2022 at 11:00 in Kobe's Zoom Room
An Internalist Approach to Correct-by-Construction Compilers

By A. Pardo, E. Gunther, M. Pagano and M. Viera

Moderator: Kobe Wullaert

Wed, Dec 15, 2021 at 11:00 in Eelco's Zoom Room
Binding as sets of scopes (follow-up)

By Matthew Flatt in ACM

Moderator: Eelco Visser

Pages 705–717

Wed, Dec 08, 2021 at 11:00 in Eelco's Zoom Room
Binding as sets of scopes

By Matthew Flatt in ACM

Moderator: Eelco Visser

Pages 705–717

Wed, Dec 01, 2021 at 11:00 in Jesper's Zoom Room
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages

By Sebastian Ullrich, Leonardo de Moura

Moderator: Jesper Cockx

Wed, Nov 10, 2021 at 11:00 in Dennis' Zoom Room
Rewrite Rule Inference Using Equality Saturation

By Chandrakana Nandi, Max Willsey, Amy Zhu, Yisu Remy Wang, Brett Saiki, Adam Anderson, Adriana Schulz, Dan Grossman, Zachary Tatlock in ACM

Moderator: Dennis Sprokholt

Wed, Nov 03, 2021 at 11:00 in Jesper's Zoom Room
How statically-typed functional programmers write code

By Justin Lubin, Sarah E. Chasins in ACM

Moderator: Jesper Cockx

Wed, Oct 27, 2021 at 11:00 in Some Zoom Room
Durable Functions: Semantics for Stateful Serverless

By Sebastian Burckhardt, Chris Gillum, David Justo, Konstantinos Kallas, Connor McMahon, Christopher S. Meiklejohn in ACM

Moderator: Asterios Katsifodimos

Wed, Oct 06, 2021 at 11:00 in Casper's Zoom Room
Compositional Programming

By Weixin Zhang, Yaozhu Sun, Bruno C. D. S. Oliveira in ACM

Moderator: Casper Bach Poulsen

Wed, Sep 29, 2021 at 11:00 in Soham's Zoom Room
Mathematizing C++ Concurrency in POPL 2011

By Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber

Moderator: Soham Chakraborty

Wed, Sep 22, 2021 at 11:00 in Arjen's Zoom Room
Quipper: a scalable quantum programming language

By Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, Benoît Valiron in ACM

Moderator: Arjen Rouvoet

Wed, Sep 15, 2021 at 11:00 in Cas' Zoom Room
How to design co-programs

By Jeremy Gibbons

Moderator: Cas van der Rest

Wed, Sep 08, 2021 at 11:00 in Jesper's Zoom Room
Wed, Sep 01, 2021 at 11:00 in Eelco's Zoom Room
Quantum internet: A vision for the road ahead

By Stephanie Wehner, David Elkouss, Ronald Hanson

Moderator: Eelco Visser

Wed, Jul 07, 2021 at 11:00 in Soham's Zoom Room
Exploring C Semantics and Pointer Provenance

By Kayvan Memarian, VictorB. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, Peter Sewell in POPL'19

Moderator: Soham Chakraborty

Wed, Jun 30, 2021 at 11:00 in Jesper's Zoom Room
MAC, A Verified Static Information-Flow Control Library

By Marco Vassena, Alejandro Russo, Pablo Buiras, Lucas Waye

Moderator: Jesper Cockx

Wed, Jun 23, 2021 at 11:00 in Dennis' Zoom Room
Adaptive Restarts for Stochastic Synthesis

By Jason R. Koenig, Oded Padon, Alex Aiken

Moderator: Dennis Sprokholt

Wed, Jun 16, 2021 at 11:00 in Arjen's Zoom Room
OutsideIn(X): Modular Type Inference with Local Assumptions

By Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, Martin Sulzmann

Moderator: Arjen Rouvoet

sections 1-4

Wed, Jun 09, 2021 at 11:00 in Casper's Zoom Room
Asynchronous Effects

By Danel Ahman, Matija Pretnar in ACM

Moderator: Casper Bach Poulsen

Wed, Jun 02, 2021 at 11:00 in Jesper's Zoom Room
Choosing is Losing: How to combine the benefits of shallow and deep embeddings through reflection

By Artjoms Šinkarovs, Jesper Cockx in Arxiv

Moderator: Jesper Cockx

Wed, May 26, 2021 at 11:00 in Peter's Zoom Room
Funcons-beta: Fundamental Constructs for Programming Languages

By Peter Mosses

Moderator: Peter Mosses

Draft of a forthcoming conference submission

Wed, May 12, 2021 at 11:00 in Cas' Zoom Room
A predicate transformer semantics for effects (functional pearl)

By Wouter Swierstra, Tim Baanen in ACM

Moderator: Cas van der Rest

Wed, Apr 28, 2021 at 11:00 in Aron's Zoom Room
Reusing Static Analysis across Different Domain-Specific Languages using Reference Attribute Grammars

By Johannes Mey, Thomas Kühn, René Schöne, Uwe Assmann

Moderator: Aron Zwaan

Wed, Mar 31, 2021 at 11:00 in Eelco's Zoom Room
Macros for domain-specific languages

By Michael Ballantyne, Alexis King, Matthias Felleisen in ACM

Moderator: Eelco Visser

Wed, Mar 24, 2021 at 11:00 in Lucas' Zoom Room
Implementing type theory in higher order constraint logic programming

By Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi

Moderator: Lucas Escot

Wed, Mar 17, 2021 at 11:00 in Bohdan's Zoom Room
Backpack: Retrofitting Haskell with Interfaces

By Scott Kilpatrick, Derek Dreyer, Simon Peyton Jones, Simon Marlow

Moderator: Bohdan Liesnikov

Wed, Mar 10, 2021 at 11:00 in Eelco's Zoom Room
Applicative functors and fully transparent higher-order modules

By Xavier Leroy

Moderator: Eelco Visser

Wed, Mar 10, 2021 at 11:00 in Eelco's Zoom Room
A modular module system

By Xavier Leroy

Moderator: Eelco Visser

Wed, Feb 17, 2021 at 11:00 in Aron's Zoom Room
A systematic approach to deriving incremental type checkers

By André Pacak, Sebastian Erdweg, Tamás Szabó in ACM

Moderator: Aron Zwaan

Wed, Feb 10, 2021 at 11:00 in Casper's Zoom Room
Program fragments, linking, and modularization

By Luca Cardelli

Moderator: Casper Bach Poulsen

Wed, Feb 03, 2021 at 11:00 in Asterios' Zoom Room
Cloud Programming Simplified: A Berkeley View on Serverless Computing

By Eric Jonas, Johann Schleier-Smith, Vikram Sreekanti, Chia-Che Tsai, Anurag Khandelwal, Qifan Pu, Vaishaal Shankar, Joao Carreira, Karl Krauth, Neeraja Yadwadkar, Joseph E. Gonzalez, Raluca Ada Popa, Ion Stoica, David A. Patterson

Moderator: Asterios Katsifodimos

Wed, Jan 13, 2021 at 11:30 in Jesper's Zoom Room
A Separation Logic for Effect Handlers

By Paulo Emílio de Vilhena, François Pottier

Moderator: Jesper Cockx

Instead of a paper, this week we will discuss two talks at POPL '21

Wed, Jan 13, 2021 at 11:00 in Jesper's Zoom Room
egg: Fast and Extensible Equality Saturation

By Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, Pavel Panchekha

Moderator: Jesper Cockx

Instead of a paper, this week we will discuss two talks at POPL '21

Wed, Jan 06, 2021 at 11:00 in Eelco's Zoom Room
Hashing Modulo Alpha-Equivalence

By Krzysztof Maziarz, Tom Ellis, Alan Lawrence, Andrew Fitzgibbon, Simon Peyton Jones

Moderator: Eelco Visser

Wed, Dec 16, 2020 at 11:00 in Arjen's Zoom Room
Dependently Typed Compilers Don't Go Wrong

By Mitchell Pickard, Graham Hutton in ACM

Moderator: Arjen Rouvoet

Wed, Dec 09, 2020 at 11:00 in Cas' Zoom Room
Effect Handlers, Evidently

Moderator: Cas van der Rest

Wed, Dec 02, 2020 at 11:00 in Eelco's Zoom Room
Concise, Type-Safe, and Efficient Structural Diffing

By Sebastian Erdweg, Tamás Szabó, André Pacak

Moderator: Eelco Visser

Wed, Nov 25, 2020 at 11:00 in Arjen's Zoom Room
Extrinsically Typed Operational Semantics for Functional Languages

By Matteo Cimini, Dale Miller, Jeremy G. Siek

Moderator: Arjen Rouvoet

Wed, Nov 11, 2020 at 11:00 in Cas's Zoom Room
Lower your guards: a compositional pattern-match coverage checker

By Sebastian Graf, Simon Peyton Jones, Ryan G. Scott in ACM

Moderator: Cas van der Rest

Wed, Nov 04, 2020 at 09:15 in Jesper's Zoom Room
Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time

By Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, Alexandra Silva in ACM

Moderator: Jesper Cockx

Wed, Oct 28, 2020 at 11:00 in Jesper's Zoom Room
Grounding Thin-Air Reads with Event Structures

By Soham Chakraborty, Viktor Vafeiadis in ACM

Moderator: Jesper Cockx

Wed, Oct 21, 2020 at 09:15 in Jesper's Zoom Room
Speculative Taint Tracking (STT): A Comprehensive Protection for Speculatively Accessed Data

By Jiyong Yu, Mengjia Yan, Artem Khyzha, Adam Morrison, Josep Torrellas, Christopher W. Fletcher in ACM

Moderator: Jesper Cockx

Wed, Oct 14, 2020 at 09:15 in Jesper's Zoom Room
High-level signatures and initial semantics

By Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi in ArXiv

Moderator: Jesper Cockx

Wed, Oct 07, 2020 at 09:15 in Jesper's Zoom Room
Practical Abstractions for Automated Verification of Message Passing Concurrency

By Wytse Oortwijn, Marieke Huisman in Springer

Moderator: Jesper Cockx

Wed, Sep 30, 2020 at 09:30 in Jesper's Zoom Room
Quantomatic: A Proof Assistant for Diagrammatic Reasoning

By Aleks Kissinger, Vladimir Zamdzhiev in Springer

Moderator: Jesper Cockx

Wed, Sep 16, 2020 at 11:00 in Jesper's Zoom Room
A dependently typed calculus with pattern matching and erasure inference

By Matúš Tejiščák in ACM

Moderator: Jesper Cockx

Wed, Sep 02, 2020 at 11:00 in Arjen's Zoom Room
Live Functional Programming with Typed Holes

By Cyrus Omar, Ian Voysey, Ravi Chugh, Matthew A. Hammer in ACM

Moderator: Arjen Rouvoet

Wed, Jun 24, 2020 at 11:00 in Eelco's Zoom Room
Wed, Jun 17, 2020 at 11:00 in Eelco's Zoom Room
Hindley-Milner Elaboration in Applicative Style: Functional Pearl.

By François Pottier in ACM

Moderator: Hendrik van Antwerpen

Wed, Jun 10, 2020 at 11:00 in Eelco's Zoom Room
Snek: Overloading Python Semantics via Virtualization

By James M. Decker, Dan Moldovan, Andrew A. Johnson, Guannan Wei, Vritant Bhardwaj, Gregory Essertel, Fei Wang, Alexander B. Wiltschko, Tiark Rompf

Moderator: Jules Jacobs

Wed, Jun 03, 2020 at 11:00 in Eelco's Zoom Room
Armada: Low-Effort Verification of High-Performance Concurrent Programs

By Jacob R. Lorch, Yixuan Chen, Manos Kapritsos, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, Xueyuan Zhao in PLDI '20

Moderator: Robbert Krebbers

Wed, May 27, 2020 at 11:00 in Eelco's Zoom Room
A Co-contextual Type Checker for Featherweight Java

By Edlira Kuci, Sebastian Erdweg, Oliver Bracevac, Andi Bejleri, Mira Mezini in Dagstuhl

Moderator: Arjen Rouvoet

Wed, May 20, 2020 at 11:00 in Eelco's Zoom Room
Generics of a Higher Kind

By Adriaan Moors, Frank Piessens, Martin Odersky in ACM

Moderator: Paolo Giarrusso

Wed, May 13, 2020 at 11:00 in Eelco's Zoom Room
Compiling pattern matching

By Lennart Augustsson in FPCA 1985

Moderator: Jeff Smits

Wed, May 06, 2020 at 11:00 in Eelco's Zoom Room
Combining Effects and Coeffects via Grading

By Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, Tarmo Uustalu in ACM

Moderator: Cas van der Rest

Skip section 5 (categorical semantics of graded (co)monads)

Wed, Apr 22, 2020 at 11:00 in Eelco's Zoom Room
Parsing Mixfix Operators

By Nils Anders Danielsson, Ulf Norell

Moderator: Paolo Giarrusso

Wed, Apr 15, 2020 at 11:00 in Eelco's Zoom Room
Bidirectional Typing

By Joshua Dunfield, Neel Krishnaswami

Moderator: Jeff Smits

Wed, Apr 08, 2020 at 11:00 in Eelco's Zoom Room
QED at Large: A Survey of Engineering of Formally Verified Software

By Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock in Cornell University

Moderator: Jesper Cockx

Page 1-40

Wed, Apr 01, 2020 at 11:00 in Eelco's Zoom Room
A very modal model of a modern, major, general type system

By Andrew W, Paul-André Melliès, Christopher D. Richards, Jérôme Vouillon in ACM SIGPLAN 2007

Moderator: Robbert Krebbers

Wed, Mar 25, 2020 at 11:00 in Eelco's Zoom Room
Quantitative Program Reasoning with Graded Modal Types

By Orchard, Dominic A. and Liepelt, Vilem and Eades, Harley in University of Kent

Moderator: Arjen Rouvoet

Wed, Mar 11, 2020 at 11:00 in Colloquiumzaal 0.E420 (Turing)
AlleAlle: bounded relational model finding with unbounded data

By Jouke Stoel, Tijs van der Storm, Jurgen J. Vinju in Onward! 2019

Moderator: Jasper Denkers

Wed, Mar 04, 2020 at 11:00 in Colloquiumzaal 0.E420 (Turing)
Finally Tagless, Partially Evaluated

By Carette, Kiselyov, Shan in APLAS 2007

Moderator: Cas van der Rest

A paper about how to embed typed languages in a typed meta-language (like Haskell or ML) without requiring fancy extensions like GADTs.

Wed, Feb 26, 2020 at 11:00 in Colloquiumzaal 0.E420 (Turing)
Stop when you are almost-full

By Vytiniotis, Coquand, Wahlstedt

Moderator: Arjen Rouvoet

A paper about termination measures. A paper that everyone (at POPL) should read according to James Mckinna ;-)

Wed, Feb 19, 2020 at 11:00 in Colloquiumzaal 0.E420 (Turing)
Binders by day, labels by night: effect instances via lexically scoped handlers

By Dariusz Biernacki, Maciej Pirog, Piotr Polesiuk, Filip Sieczkowski

Moderator: Casper Bach Poulsen

Algebraic effects, POPL 2020 paper

Wed, Feb 12, 2020 at 11:00 in Colloquiumzaal 0.E420 (Turing)
Theorems for Free!

By Philip Wadler in FPCA '89

Moderator: Jesper Cockx

Wed, Feb 05, 2020 at 11:00 in Colloquiumzaal 0.E420 (Turing)
Tabled Typeclass Resolution

By Daniel Selsam, Sebastian Ullrich, Leonardo de Moura

Moderator: Robbert Krebbers

Wed, Jan 29, 2020 at 11:00 in Colloquiumzaal 0.E420 (Turing)
Wed, Jan 22, 2020 at 11:00 in Colloquiumzaal 0.E420 (Turing)
Resources, Concurrency and Local Reasoning

By Peter O’Hearn in Theoretical Computer Science 375(1-3), 271-307, 2007

Moderator: Jesper Cockx

We will discuss sections 1-7 (pages 1-24)

Wed, Jan 15, 2020 at 11:00 in Colloquiumzaal 0.E420 (Turing)
When Code Completion Fails: A Case Study on Real-World Completions

By Vincent J. Hellendoorn, Sebastian Proksch, Harald C. Gall, and Alberto Bacchelli in ICSE 2019

Moderator: Daniel Pelsmaeker

Wed, Jan 08, 2020 at 11:00 in Colloquiumzaal 0.E420 (Turing)
Monad Transformers and Modular Algebraic Effects: What Binds Them Together

By Tom Schrijvers, Maciej Piróg, Nicolas Wu, and Mauro Jaskelioff in Haskell 2019

Moderator: Casper Bach Poulsen

Wed, Dec 18, 2019 at 11:00 in Colloquiumzaal 0.E420 (Turing)
How to Believe a Machine-Checked Proof

By Robert Pollack in BRICS 1997

Moderator: Jesper Cockx

Wed, Dec 11, 2019 at 11:00 in Colloquiumzaal 0.E420 (Turing)
Wed, Dec 04, 2019 at 11:00 in Colloquiumzaal 0.E420 (Turing)
Capture-Avoiding and Hygienic Program Transformations

By Sebastian Erdweg, Tijs van der Storm, Yi Dai in ECOOP 2014

Moderator: Eelco Visser

Wed, Nov 27, 2019 at 11:00 in Colloquiumzaal 0.E420 (Turing)
Deadlock-Free Monitors

By Jafar Hamin and Bart Jacobs in ESOP 2018

Moderator: Jules Jacobs

Wed, Nov 06, 2019 at 11:00 in De Bruijn
Sequential Effect Systems with Control Operators

By Colin S. Gordon

Moderator: Eelco Visser

Wed, Oct 30, 2019 at 11:00 in Colloquiumzaal 0.E420 (Turing)
Next-Paradigm Programming Languages: What Will They Look Like and What Changes Will They Bring?

By Yannis Smaragdakis in Onward 2019

Moderator: Eelco Visser

See also the video of the talk at https://www.youtube.com/watch?v=iwOFK6M1gG8

Wed, Oct 16, 2019 at 11:00 in De Bruijn
Staged Generic Programming

By Jeremy Yallop in ICFP'17

Moderator: Jeff Smits

Question: Can we apply this idea to generic traversals in Stratego?

Wed, Sep 25, 2019 at 11:00 in De Bruijn
A Path To DOT: Formalizing Fully-Path-Dependent Types

By Marianna Rapoport, Ondřej Lhoták in OOPSLA'19

Moderator: Paolo Giarrusso

We will focus not on the safety proofs, but on the language itself. In particular, I’d probably skip, at a first read, Sec. 2.3, 3.6, 5.1 and 5.2.

Wed, May 22, 2019 at 11:00 in De Bruijn
A Logic Programming Language with Finite Sets

By Agostino Dovier et al

Moderator: Arjen Rouvoet

Particularly interested in comparing sets with scopes in Statix

Wed, May 15, 2019 at 11:00 in De Bruijn
What are principal typings and what are they good for?

By Trevor Jim in POPL 1996

Moderator: Jeff Smits / Paolo Giarrusso

Of particular interest: Section 4 on separate compilation

Wed, Apr 24, 2019 at 11:00 in De Bruijn
A Foundation for Flow-Based Program Matching. Using Temporal Logic and Model Checking

By Julien Brunel, Damien Doligez, Rene Rydhof Hansen, Julia L. Lawall, Gilles Muller in POPL 2009

Moderator: Eelco Visser / Casper Bach Poulsen

Thu, Apr 04, 2019 at 11:00 in De Bruijn
Substructural Type Systems

By David Walker in Chapter 1 of Advanced Topics in Types and Programming Languages

Moderator: Eelco Visser (Andrew Tolmach)

Question: How are substructural type systems declaratively specified and how can we turn that into type checkers? How do these type systems fit in the scope graphs and Statix approach?

Wed, Mar 27, 2019 at 11:00 in 0.E420 Colloquiumzaal (Turing)
A Gentle Introduction to Multiparty Asynchronous Session Types

By Mario Coppo, Mariangiola Dezani-Ciancaglini, Luca Padovani, Nobuko Yoshida in International School on Formal Methods for the Design of Computer, Communication and Software Systems (SFM 2015) Formal Methods for Multicore Programming pp 146-178

Moderator: Sung-Shik Jongmans

Sung-Shik is visiting and will guest moderate this session

Wed, Mar 20, 2019 at 11:00 in De Bruijn
Wed, Mar 13, 2019 at 11:00 in De Bruijn
Knowing When to Ask

Moderator: Arjen

Draft paper

Wed, Feb 27, 2019 at 11:00 in De Bruijn
Wed, Feb 20, 2019 at 11:00 in De Bruijn
Wed, Feb 13, 2019 at 11:00 in De Bruijn
Modula-2 and Oberon

Moderator: Jeff

Wed, Feb 06, 2019 at 11:00 in De Bruijn
Monadic Constraint Programming

Moderator: Hendrik

Wed, Jan 30, 2019 at 11:00 in De Bruijn
Wed, Jan 23, 2019 at 11:00 in De Bruijn
Wed, Jan 16, 2019 at 11:00 in De Bruijn
Wed, Dec 05, 2018 at 11:00 in De Bruijn

Moderator: Robbert

Wed, Nov 28, 2018 at 11:00 in De Bruijn
Bindings as sets of scopes

Moderator: Arjen

Wed, Nov 21, 2018 at 11:00 in De Bruijn
Wed, Nov 14, 2018 at 11:00 in De Bruijn
Efficient and flexible incremental parsing

Moderator: Maarten Sijm (+ Eelco)

Wed, Nov 07, 2018 at 11:00 in De Bruijn
No reading group (SPLASH)
Wed, Oct 31, 2018 at 11:00 in De Bruijn
Robust projectional editing

Moderator: Daniel

Wed, Oct 24, 2018 at 11:00 in De Bruijn
Colored local type inference

Moderator: Casper

Wed, Oct 17, 2018 at 11:00 in De Bruijn
Wed, Oct 10, 2018 at 11:00 in De Bruijn
Wed, Oct 03, 2018 at 11:00 in De Bruijn
Wed, Sep 26, 2018 at 11:00 in De Bruijn
ML in ATAPL

Moderator: Eelco

Wed, Sep 19, 2018 at 11:00 in De Bruijn
Ornamental algebras,algebraic ornaments,C. McBride

Moderator: Arjen

Wed, Sep 12, 2018 at 11:00 in De Bruijn
Wed, Sep 05, 2018 at 11:00 in De Bruijn
Wed, Jun 13, 2018 at 11:00 in De Bruijn
We should Stop Claiming Generality in our Domain-Specific Language Papers

Moderator: Daco

Wed, May 30, 2018 at 11:00 in De Bruijn
Wed, May 23, 2018 at 11:00 in De Bruijn
Wed, May 16, 2018 at 11:00 in De Bruijn
Wed, May 09, 2018 at 11:00 in De Bruijn
Wed, May 02, 2018 at 11:00 in De Bruijn
Wed, Apr 25, 2018 at 11:00 in De Bruijn
Bonsai: Synthesis-Based Reasoning for Type Systems

Moderator: Eelco

Wed, Apr 04, 2018 at 11:00 in De Bruijn
Natural and Flexible Error Recovery for Generated Modular Language Environments

Moderator: Jasper

Wed, Mar 28, 2018 at 11:00 in De Bruijn
Wed, Mar 21, 2018 at 11:00 in De Bruijn
Wed, Mar 14, 2018 at 11:00 in De Bruijn
Wed, Mar 07, 2018 at 11:00 in De Bruijn
Wed, Feb 28, 2018 at 11:00 in De Bruijn
Visit by Wouter Swierstra and Victor Miraldo from Utrecht,seminar talk by Victor
Wed, Feb 21, 2018 at 11:00 in De Bruijn
Wed, Feb 14, 2018 at 11:00 in De Bruijn
Wed, Feb 07, 2018 at 11:00 in De Bruijn
Wed, Jan 31, 2018 at 11:00 in De Bruijn
Wed, Jan 24, 2018 at 11:00 in De Bruijn
Defense Jasper
Wed, Jan 17, 2018 at 11:00 in De Bruijn

Moderator: Tamas

Wed, Dec 20, 2017 at 11:00 in De Bruijn
Wed, Dec 13, 2017 at 11:00 in De Bruijn
Practical Partial Evaluation for High-Performance Dynamic Language Runtimes

Moderator: Guido

Wed, Dec 06, 2017 at 11:00 in De Bruijn
Wed, Nov 29, 2017 at 11:00 in De Bruijn

Moderator: Arjen

Wed, Nov 22, 2017 at 11:00 in De Bruijn
Wed, Nov 15, 2017 at 11:00 in De Bruijn
Wed, Nov 08, 2017 at 11:00 in De Bruijn
Spores: A Type-Based Foundation for Closures in the Age of Concurrency and Distribution

Moderator: Eelco

Wed, Nov 01, 2017 at 11:00 in De Bruijn
Sven
Wed, Oct 18, 2017 at 11:00 in De Bruijn
Wed, Oct 11, 2017 at 11:00 in De Bruijn
Restricting Grammars with Tree Automata

Moderator: Eduardo

Wed, Oct 04, 2017 at 11:00 in De Bruijn
Wed, Sep 27, 2017 at 11:00 in De Bruijn
Do Be Do Be Do

Moderator: Casper

Wed, Sep 20, 2017 at 11:00 in De Bruijn
Wed, Sep 13, 2017 at 11:00 in De Bruijn
POSTPONED

Moderator: Arjen

http://gupta.xor.ucsd.edu/site/pubs/Kundu_PLDI09.pdf

Wed, Jun 28, 2017 at 11:00 in De Bruijn
Wed, May 31, 2017 at 11:00 in De Bruijn
Wed, May 24, 2017 at 11:00 in De Bruijn
Wed, May 17, 2017 at 11:00 in De Bruijn
Wed, May 10, 2017 at 11:00 in De Bruijn
A Program Optimization for Automatic Database Result Caching

Moderator: Daco

Wed, May 03, 2017 at 11:00 in De Bruijn
Modules,abstraction,and parametric polymorphism

Moderator: Eelco

Wed, Apr 26, 2017 at 11:00 in De Bruijn
Wed, Apr 19, 2017 at 11:00 in De Bruijn
No reading group,talk by Sylvia Grewe
Wed, Apr 12, 2017 at 11:00 in De Bruijn
No reading group,OOPSLA deadline
Wed, Apr 05, 2017 at 11:00 in De Bruijn
Beginner’s Luck: A language for property-based generators

Moderator: Hendrik

Wed, Mar 29, 2017 at 11:00 in De Bruijn
No reading group,talk by Eelco
Wed, Mar 22, 2017 at 11:00 in De Bruijn
Dijkstra Monads for Free

Moderator: Robbert

Wed, Mar 15, 2017 at 11:00 in De Bruijn
Type Directed Compilation of Row-Typed Algebraic Effects

Moderator: Casper

Wed, Mar 08, 2017 at 11:00 in De Bruijn
Wed, Mar 01, 2017 at 11:00 in De Bruijn
Type soundness proofs with definitional interpreters

Moderator: Arjen

Wed, Feb 22, 2017 at 11:00 in De Bruijn
A Posteriori Environment Analysis with Pushdown Delta CFA

Moderator: Jeff

Wed, Feb 08, 2017 at 11:00 in De Bruijn
LMS-Verify: abstraction without regret for verified systems programming

Moderator: Michael

Wed, Feb 01, 2017 at 11:00 in De Bruijn
Wed, Dec 21, 2016 at 11:00 in De Bruijn
Wed, Dec 14, 2016 at 11:00 in De Bruijn
Wed, Dec 07, 2016 at 11:00 in De Bruijn
Wed, Nov 30, 2016 at 11:00 in De Bruijn
Wed, Nov 23, 2016 at 11:00 in De Bruijn
Calculating correct compilers

Moderator: Casper

Wed, Nov 16, 2016 at 11:00 in De Bruijn
Thu, Nov 10, 2016 at 11:00 in De Bruijn
Thu, Oct 27, 2016 at 11:00 in De Bruijn
Thu, Oct 20, 2016 at 11:00 in De Bruijn
Thu, Oct 13, 2016 at 11:00 in De Bruijn
Thu, Oct 06, 2016 at 11:00 in De Bruijn
Thu, Sep 29, 2016 at 11:00 in De Bruijn
Thu, Sep 22, 2016 at 11:00 in De Bruijn
Thu, Sep 15, 2016 at 11:00 in De Bruijn
Thu, Sep 08, 2016 at 11:00 in De Bruijn
Thu, Sep 01, 2016 at 11:00 in De Bruijn
Thu, Aug 25, 2016 at 11:00 in De Bruijn
Refactoring Using Type Constraints

Moderator: Sebastian

Thu, Jul 07, 2016 at 11:00 in De Bruijn
Thu, Jun 23, 2016 at 11:00 in De Bruijn
Self: The Power of Simplicity

Moderator: Hendrik

Thu, Jun 16, 2016 at 11:00 in De Bruijn
Thu, Jun 09, 2016 at 11:00 in De Bruijn
Thu, Jun 02, 2016 at 11:00 in De Bruijn
Thu, May 26, 2016 at 11:00 in De Bruijn
Thu, May 19, 2016 at 11:00 in De Bruijn
Wed, May 11, 2016 at 11:00 in De Bruijn
The K Primer (version 3.3)

Moderator: Casper

Tue, May 03, 2016 at 11:00 in De Bruijn
Tue, Apr 26, 2016 at 11:00 in De Bruijn
Tue, Apr 19, 2016 at 11:00 in De Bruijn
Tue, Apr 12, 2016 at 11:00 in De Bruijn
iThreads: A threading library for parallel incremental computation

Moderator: Sebastian

As the authors themselves suggest,we should skip Section 3.