# 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:

- The material should be PL related.
- 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

##### 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

##### 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

##### Histogram: You have to know the past to understand the present

By Tomas Petricek

Moderator: Alex Chichigin

##### 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

##### 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

##### Monad transformers and modular interpreters

By Sheng Liang, Paul Hudak, Mark Jones in ACM

Moderator: Cas van der Rest

##### Effective Extensible Programming: Unleashing Julia on GPUs

By Tim Besard, Christophe Foket, Bjorn De Sutter

Moderator: Alex Chichigin

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

##### 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

##### An Internalist Approach to Correct-by-Construction Compilers

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

Moderator: Kobe Wullaert

##### Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages

By Sebastian Ullrich, Leonardo de Moura

Moderator: Jesper Cockx

##### 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

##### How statically-typed functional programmers write code

By Justin Lubin, Sarah E. Chasins in ACM

Moderator: Jesper Cockx

##### 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

##### Compositional Programming

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

Moderator: Casper Bach Poulsen

##### Mathematizing C++ Concurrency in POPL 2011

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

Moderator: Soham Chakraborty

##### 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

##### Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl)

By Adam Chlipala in ACM

Moderator: Jesper Cockx

##### Quantum internet: A vision for the road ahead

By Stephanie Wehner, David Elkouss, Ronald Hanson

Moderator: Eelco Visser

##### 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

##### MAC, A Verified Static Information-Flow Control Library

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

Moderator: Jesper Cockx

##### Adaptive Restarts for Stochastic Synthesis

By Jason R. Koenig, Oded Padon, Alex Aiken

Moderator: Dennis Sprokholt

##### OutsideIn(X): Modular Type Inference with Local Assumptions

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

Moderator: Arjen Rouvoet

sections 1-4

##### 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

##### Funcons-beta: Fundamental Constructs for Programming Languages

By Peter Mosses

Moderator: Peter Mosses

Draft of a forthcoming conference submission

##### A predicate transformer semantics for effects (functional pearl)

By Wouter Swierstra, Tim Baanen in ACM

Moderator: Cas van der Rest

##### 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

##### Macros for domain-specific languages

By Michael Ballantyne, Alexis King, Matthias Felleisen in ACM

Moderator: Eelco Visser

##### Implementing type theory in higher order constraint logic programming

By Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi

Moderator: Lucas Escot

##### Backpack: Retrofitting Haskell with Interfaces

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

Moderator: Bohdan Liesnikov

##### Applicative functors and fully transparent higher-order modules

By Xavier Leroy

Moderator: Eelco Visser

##### A systematic approach to deriving incremental type checkers

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

Moderator: Aron Zwaan

##### 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

##### 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

##### 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

##### Hashing Modulo Alpha-Equivalence

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

Moderator: Eelco Visser

##### Dependently Typed Compilers Don't Go Wrong

By Mitchell Pickard, Graham Hutton in ACM

Moderator: Arjen Rouvoet

##### Effect Handlers, Evidently

Moderator: Cas van der Rest

##### Concise, Type-Safe, and Efficient Structural Diffing

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

Moderator: Eelco Visser

##### Extrinsically Typed Operational Semantics for Functional Languages

By Matteo Cimini, Dale Miller, Jeremy G. Siek

Moderator: Arjen Rouvoet

##### 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

##### 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

##### Grounding Thin-Air Reads with Event Structures

By Soham Chakraborty, Viktor Vafeiadis in ACM

Moderator: Jesper Cockx

##### 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

##### High-level signatures and initial semantics

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

Moderator: Jesper Cockx

##### Practical Abstractions for Automated Verification of Message Passing Concurrency

By Wytse Oortwijn, Marieke Huisman in Springer

Moderator: Jesper Cockx

##### Quantomatic: A Proof Assistant for Diagrammatic Reasoning

By Aleks Kissinger, Vladimir Zamdzhiev in Springer

Moderator: Jesper Cockx

##### A dependently typed calculus with pattern matching and erasure inference

By Matúš Tejiščák in ACM

Moderator: Jesper Cockx

##### Live Functional Programming with Typed Holes

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

Moderator: Arjen Rouvoet

##### Prototyping a Functional Language using Higher-Order Logic Programming: A Functional Pearl on Learning the Ways of λProlog/Makam

By Antonis Stampoulis, Adam Chlipala in ACM

Moderator: Jesper Cockx

##### Hindley-Milner Elaboration in Applicative Style: Functional Pearl.

By François Pottier in ACM

Moderator: Hendrik van Antwerpen

##### 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

##### 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

##### A Co-contextual Type Checker for Featherweight Java

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

Moderator: Arjen Rouvoet

##### Generics of a Higher Kind

By Adriaan Moors, Frank Piessens, Martin Odersky in ACM

Moderator: Paolo Giarrusso

##### 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)

##### 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

##### 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

##### Quantitative Program Reasoning with Graded Modal Types

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

Moderator: Arjen Rouvoet

##### AlleAlle: bounded relational model finding with unbounded data

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

Moderator: Jasper Denkers

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

##### 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 ;-)

##### 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

##### Tabled Typeclass Resolution

By Daniel Selsam, Sebastian Ullrich, Leonardo de Moura

Moderator: Robbert Krebbers

##### 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)

##### 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

##### 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

##### On the meaning of the logical constants and the justification of the logical laws

By Per Martin Lof

Moderator: Arjen Rouvoet

##### Capture-Avoiding and Hygienic Program Transformations

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

Moderator: Eelco Visser

##### 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

##### Staged Generic Programming

By Jeremy Yallop in ICFP'17

Moderator: Jeff Smits

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

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

##### A Logic Programming Language with Finite Sets

By Agostino Dovier et al

Moderator: Arjen Rouvoet

Particularly interested in comparing sets with scopes in Statix

##### 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

##### 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

##### 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?

##### 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

##### A Refactoring Constraint Language and Its Application to Eiffel

Moderator: Daniel

##### Knowing When to Ask

Moderator: Arjen

Draft paper

##### Design science in information systems research

Moderator: Jasper

##### New requirement for data sharing

Moderator: Eelco

##### Modula-2 and Oberon

Moderator: Jeff

##### Monadic Constraint Programming

Moderator: Hendrik

##### Five Misunderstandings About Case-Study Research

Moderator: Peter

##### Relative Store Fragments for Singleton Abstraction

Moderator: Sven

Moderator: Robbert

##### Bindings as sets of scopes

Moderator: Arjen

##### Efficient and flexible incremental parsing

Moderator: Maarten Sijm (+ Eelco)

##### No reading group (SPLASH)

##### Robust projectional editing

Moderator: Daniel

##### Colored local type inference

Moderator: Casper

##### Incremental Computation with Names (Nominal Adapton)

Moderator: Gabriel

##### αProlog: A Logic Programming Language with Names,Binding and α-Equivalence

Moderator: Hendrik

##### Specializing a meta-interpreter: JIT compilation of dynsem specifications on the graal VM

Moderator: Eelco/Arjen

##### ML in ATAPL

Moderator: Eelco

##### Ornamental algebras,algebraic ornaments,C. McBride

Moderator: Arjen

##### The use of program dependence graphs in software engineering

Moderator: Jeff

##### Defensive Points-To Analysis: Effective Soundness via Laziness

Moderator: Sven

##### We should Stop Claiming Generality in our Domain-Specific Language Papers

Moderator: Daco

##### Composing dataflow analyses and transformations

Moderator: Jeff

##### Inferring Scope Through Syntactic Sugar

Moderator: Hendrik

##### Build Systems à la Carte (under review)

Moderator: Gabriel

##### Complete and Easy Bidrectional Typechecking for Higher-Rank Polymorphism

Moderator: Casper

##### Bonsai: Synthesis-Based Reasoning for Type Systems

Moderator: Eelco

##### Natural and Flexible Error Recovery for Generated Modular Language Environments

Moderator: Jasper

##### Programming type-safe transformations using higher-order abstract syntax

Moderator: Sebastian

##### Demand-driven incremental object queries

Moderator: Daco

##### Doctoral Regulations & Implementation Decree 2018

Moderator: Eelco

##### Visit by Wouter Swierstra and Victor Miraldo from Utrecht,seminar talk by Victor

##### Coeffects: Unified Static Analysis of Context-Dependence

Moderator: Peter

##### Verifying Efficient Function Calls in CakeML

Moderator: Arjen

##### CDuce: An XML-Centric General-Purpose Language

Moderator: Jeff

##### Defense Jasper

Moderator: Tamas

##### Practical Partial Evaluation for High-Performance Dynamic Language Runtimes

Moderator: Guido

##### Needle & Knot: Binder boilerplate tied up

Moderator: Casper

Moderator: Arjen

##### Bringing the Web up to Speed with WebAssembly

Moderator: Robbert

##### A calculus for constraint-based flow typing

Moderator: Jeff

##### Spores: A Type-Based Foundation for Closures in the Age of Concurrency and Distribution

Moderator: Eelco

##### Sven

##### Restricting Grammars with Tree Automata

Moderator: Eduardo

##### Constraint handling rules with binders,patterns and generic quantification

Moderator: Hendrik

##### Do Be Do Be Do

Moderator: Casper

##### Persistence for the masses: RRB-vectors in a systems language

Moderator: Michael

##### Typed Architectures: Architectural Support for Lightweight Scripting

Moderator: Gabriel

##### Operator precedence for data-dependent grammars

Moderator: Peter

##### Generalising monads to arrows

Moderator: Sven

##### Why Don’t Software Developers Use Static Analysis Tools to Find Bugs?

Moderator: Sebastian

##### A Program Optimization for Automatic Database Result Caching

Moderator: Daco

##### Modules,abstraction,and parametric polymorphism

Moderator: Eelco

##### Efficient and flexible incremental parsing

Moderator: Eduardo

##### No reading group,talk by Sylvia Grewe

##### No reading group,OOPSLA deadline

##### Beginner’s Luck: A language for property-based generators

Moderator: Hendrik

##### No reading group,talk by Eelco

##### Dijkstra Monads for Free

Moderator: Robbert

##### Type Directed Compilation of Row-Typed Algebraic Effects

Moderator: Casper

##### Units: Cool Modules for HOT Languages

Moderator: Gabriel

##### Type soundness proofs with definitional interpreters

Moderator: Arjen

##### A Posteriori Environment Analysis with Pushdown Delta CFA

Moderator: Jeff

##### LMS-Verify: abstraction without regret for verified systems programming

Moderator: Michael

##### Polymorphism,subtyping,and type inference in MLsub

Moderator: Peter

##### ADAPTON: Composable,Demand- Driven Incremental Computation

Moderator: Daco

##### Abstract Interpretation Frameworks

Moderator: Sven

##### Modular interpreters with implicit context propagation

Moderator: Vlad

##### Reachability and error diagnosis in LR(1) parsers

Moderator: Eduardo

##### Calculating correct compilers

Moderator: Casper

##### Hazelnut: A Bidirectionally Typed Structure Editor Calculus

Moderator: Sebastian

##### A Practical Framework for Type Inference Error Explanation

Moderator: Hendrik

##### Galois Transformers and Modular Abstract Interpreters

Moderator: Sven

##### Modular Verification for Computer Security

Moderator: Robbert

##### Language parametric module management for IDEs

Moderator: Gabriel

##### Alias annotations for program understanding

Moderator: Jeff

##### Towards a Universal Code Formatter through Machine Learning

Moderator: Eduardo

##### Set-theoretic foundation of parametric polymorphism and subtyping

Moderator: Peter

##### Dag-Calculus: A Calculus for Parallel Computation

Moderator: Andrew

##### Refactoring Using Type Constraints

Moderator: Sebastian

##### Datalog and Recursive Query Processing

Moderator: Daco

##### Self: The Power of Simplicity

Moderator: Hendrik

##### The Calculational Design of a Generic Abstract Interpreter

Moderator: Sven

##### Axiomatic bootstrapping: a guide for compiler hackers

Moderator: Gabriel

##### Tracing vs. Partial Evaluation

Moderator: Vlad

##### Lightweight Verification of Separate Compilation

Moderator: Robbert

##### The K Primer (version 3.3)

Moderator: Casper

##### Error explanation with distance metrics

Moderator: Jeff

##### Hygienic Resugaring of Compositional Desugaring

Moderator: Eelco

##### Coinductive big-step operational semantics

Moderator: Andrew

##### iThreads: A threading library for parallel incremental computation

Moderator: Sebastian

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