# Reading Group

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

How the reading group works:

- all participants read the paper in advance
- at the start, the moderator makes a round collecting questions from the participants (without discussion)
- then we discuss those questions, typically in order of the section in the paper that they relate to

Add entries to `_data/reading-group.yml`

##### Hashing Modulo Alpha-Equivalence

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

Moderator: Eelco Visser

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

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

## Past Sessions

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