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

.

##### Functional Pearl: Heterogeneous random-access lists

By Wouter Swierstra in Journal of Functional Programming

Moderator: Lucas Escot / Jesper Cockx

## Past Sessions

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

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

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

##### Coq à la carte: a practical approach to modular syntax with binders

By Yannick Forster, Kathrin Stark

Moderator: Bohdan Liesnikov

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

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

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

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

##### Data-Codata Symmetry and its Interaction with Evaluation Order

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

Moderator: Jaro Reinders

##### Supercompilation by Evaluation

By Maximilian Bolingbroke, Simon Peyton Jones

Moderator: Dennis Sprokholt

##### Controlling Unfolding in Type Theory

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

Moderator: Jesper Cockx

##### A Tutorial on Graph Transformation

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

Moderator: Luka Miljak

##### Future Directions for Optimizing Compilers

By Nuno P. Lopes, John Regehr

Moderator: Dennis Sprokholt

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