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.
Principles of Educational Programming Language Design
By Michael Kölling in Informatics in Education
Moderator: Jaro Reinders
The paper is light, so please read the whole thing.
Past Sessions
The Long Way to Deforestation
By Yijia Chen and Lionel Parreaux in ICFP 2024
Moderator: Jaro Reinders
Please read S1 and S2. I will focus mainly on S3 and S5 (I'll skip S4).
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
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)
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.
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.
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!
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
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.
Synthesizing Abstract Transformers
By Pankaj Kumar Kalita, Sujit Kumar Muduli, Loris D'Antoni, Thomas Reps and Subhajit Roy
Moderator: Dennis Sprokholt
ITrees
By Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce and Steve Zdancewic
Moderator: Casper Bach Poulsen
Reasoning about Effect Interaction by Fusion
By Zhixuan Yang and Nicolas Wu
Moderator: Casper Bach Poulsen
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
Tabled Typeclass Resolution
By Daniel Selsam, Sebastian Ullrich, Leonardo de Moura in arxiv
Moderator: Bohdan Liesnikov
Automating Program Transformation with Coccinelle
By Julia Lawall and Gilles Muller in NFM 2022
Moderator: Layne Liu
One Parser to Rule Them All
By Ali Afroozeh and Anastasia Izmaylova in Onward! 2015
Moderator: Jaro Reinders
Backpack: Retrofitting Haskell with Interfaces
By Scott Kilpatrick, Derek Dreyer, Simon Peyton Jones and Simon Marlow in POPL14
Moderator: Cas van der Rest
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
Calculating Compilers Categorically
By Conal Elliott in Unpublished draft
Moderator: Cas van der Rest
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
Functional Pearl: Heterogeneous random-access lists
By Wouter Swierstra in Journal of Functional Programming
Moderator: Lucas Escot / Jesper Cockx
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.