• When and where? We meet on Wednesday 10:00, (roughly) every two weeks, alternating between MFF and FIT
• Email updates Sign up here to receive email updates about meetings.
• What paper? Post ideas and vote using Github issues!

• What: Understanding and Finding JIT Compiler Performance Bugs by Zijian Yi, Cheng Ding, August Shi and Milos Gligoric
• Paper: https://dl.acm.org/doi/abs/10.1145/3798245
• Where: Room TH-A:942, Thákurova 9, Praha 6 (see a guide and a map)
• Who: Pierre Donat-Bouillud
• Comment: JIT compilers might have software bugs, and fuzzing, especially differential fuzzing, has often been used to find those bugs (mostly in JS engines). This article shows how differential testing can be used to find performance bugs in a JIT compiler, and not only compilation performance bugs but also runtime performance bugs. This is demonstrated on 2 Java JIT compilers, Oracle Hotspot and Graal. Sections 3 to 5 describe an empirical study of performance bugs in the 2 java compilers and on 2 JS JIT compilers. Section 6 has the actual differential performance testing algorithm.

What: Chains of Meaning in the STEPS System by Ian Piumarta, VPRI Internal Memo 2009
PDF
Where: S204 (corridor in front of), Malostranské nám. 25 (see a map and a building plan)
Who: Joel Jakubovic
Comment: "STEPS Towards New Computing" was a US NSF-funded project 2007-2012 to reduce the bulk of the personal computing tech stack to under 20,000 lines of code (in as many domain-specific languages as would achieve this). This memo illustrates the idea of a STEPS "Chain of Meaning" (CoM) using a complete example that converts a textual representation of abstract syntax trees into executable native code for the Intel 386. Simplicity and clarity at each stage in the chain are the primary goals of this example CoM.
Why are you interested in it or why should it be a good idea? It's a concrete example of the OMeta meta-DSL for rapidly prototyping ad-hoc domain-specific languages. The design of OMeta in the Appendix is an interesting case of compressing all the main DSL tasks into a single notation (freely mixing the parsing of concrete syntax, the parsing of abstract structures, and the compilation/execution thereof). I wonder what relation it has to parser combinators. I also wonder how to generalise the idea to more general notations that aren't necessarily textual, and why OMeta's successor Ohm decided to split the "semantic actions" from the "parsing".

Note that because I found the memo's presentation choices a bit annoying, I wrote notes in a blog post that I wish I could have read first.

• What: The implicit calculus: a new foundation for generic programming by Bruno C.d.S. Oliveira, Tom Schrijvers, Wontae Choi, Wonchan Lee, Kwangkeun Yi
• Paper: https://dl.acm.org/doi/10.1145/2254064.2254070
• Where: Room TH-A-1435, Thákurova 9, Praha 6 (see a guide and a map)
• Who: Tianyao Zhou
• Comment: This paper formally captures the Scala's implicit in a core calculus. Novelty of this calculus is partial resolution and higher-order implicit rules. The implicit calculus provides a formal model of implicits, which can be used by language designers to study and inform implementations of similar mechanisms in their own languages. Reading section 1 and 2 is enough to understand the basic ideas. Section 3-5 are more detailed. Section 3 is the formal definition of this calculus. Section 4 is about implementing the calculus in a System F language. Section 5 says the calculus can be used to implement generic programming in a source language. We recommend reading sections 1 and 2 and having a look at section 3.

• What: AST vs. Bytecode: Interpreters in the Age of Meta-Compilation by Octave Larose, Sophie Kaleba, Humphrey Burchell and Stefan Marr 2023
• Paper: https://dl.acm.org/doi/pdf/10.1145/3622808
• Where: Room T9:346, Thákurova 9, Praha 6 (see a guide and a map)
• Who: Vojtěch Březina
• Comment: Thanks to partial evaluation and meta-tracing, it became practical to build language implementations that reach state-of-the-art peak performance by implementing only an interpreter. Folklore tells us that bytecode interpreters are superior to abstract-syntax-tree (AST) interpreters both in terms of memory use and run-time performance. While metacompilers don't seem too widespread yet, it is interesting to look at how using them changes what a performant implementation looks like. As always with interpreter papers, there are some ways we can try to relate the findings to R. The paper also gives some basic insights into general programming language design. For the rest of the group, they will probably not be that interesting, but since I am still quite new to this field, I hope to start a discussion on some of them. I would recommend everyone else read at least sections 2 and 5, since sections 3 and 4 focus mainly on the used metodology.

• What: Interaction Substrates: Combining Power and Simplicity in Interactive Systems, Wendy E. Mackay, Michel Beaudouin-Lafon
• Paper: https://dl.acm.org/doi/full/10.1145/3706598.3714006
• Where: S204 (corridor in front of), Malostranské nám. 25 (see a map and a building plan)
• Who: Tomas Petricek
• Comment: The paper presents an alternative to the typical interfaces of modern software systems - which are either simple but limited, or powerful but complex. The idea is to structure systems in terms of substrates that users can interact with and manipulate. Let's try to read sections 1-4, which provide an overview of the idea. Sections 5 and 6 are interesting as they perform rigorous evaluation in terms of human-computer interaction, which may be interesting to discuss too if we have time. (The paper specifically does not look at programming environments, but this is the reason why I find it interesting for our reading group!)

• What: Float Self-Tagging by Olivier Melançon, Manuel Serrano, Marc Feeley
• Paper: https://arxiv.org/abs/2411.16544
• Where: Room T9:346, Thákurova 9, Praha 6 (see a guide and a map)
• Who: Matěj Kocourek
• Comment: An interesting aspect of self-tagging is that it exploits the fact that floating-point numbers are not uniformly distributed in real programs, so some bit patterns can be repurposed to store type information directly inside the number. This allows both the value and its type to fit into a single machine word without heap allocation, which can significantly improve performance in dynamic languages. Compared to NaN-boxing and pointer tagging, self-tagging combines their advantages while reducing their drawbacks. Experiments show that this approach can eliminate heap allocation for almost all floating-point numbers with negligible impact on overall program performance.

• What: Proof Assistants for Teaching: a Survey, by Frédéric Tran Minh, Laure Gonnord & Julien Narboux
• Paper: https://arxiv.org/pdf/2505.13472
• Where: S204 (corridor in front of), Malostranské nám. 25 (see a map and a building plan)
• Who: Sidney Congard, Jan Liam Verter & Tomas Petricek
• Comment: We are interested in making sense of the different kinds of automatic theorem provers and dependently typed languages. This paper is a survey focused on the use of theorem provers in education, which is one interesting angle! It can be also interesting if we wanted to use some theorem provers in teaching ourselves. This is a relatively accessible paper and is not too long (16 pages, with lots of pictures and not many typing rules!), so we encourage attendees to read the entire paper.

• What: The Simple Essence of Algebraic Subtyping, Principal Type Inference with Subtyping Made Easy (Functional Pearl), by Lionel Parreaux
• Paper: https://infoscience.epfl.ch/server/api/core/bitstreams/afe084e0-0050-4542-99c7-c499d2fe1620/content
• Where: Room T9:346, Thákurova 9, Praha 6 (see a guide and a map)
• Who: Oliver Tušla
• Comment: Traditionally, it was believed that global type inference in the presence of subtyping yields complex, unwieldy types. The MLsub type inference extends traditional Hindley-Milner type inference with subtyping while preserving compact principal types. It alleviates these concerns and produces compact types that are understandable to programmers. However, MLsub is a very complex system that even experienced implementors struggle to grasp. In this paper, Parreaux proposes Simple-sub, a distillation of MLsub to a much simpler algorithm that generates the same results. For the meeting, read section 1 for the introduction on the topic, and section 2.1 for background on MLsub. We will focus on sections 3 and 4, discussing the Simple-sub design and implementation.

• What: Python 3 types in the wild: a tale of two type systems, by Ingkarat Rak-amnouykit, Daniel McCrevan, Ana Milanova, Martin Hirzel, and Julian Dolby
• Paper: https://dl.acm.org/doi/10.1145/3426422.3426981
• Where: Room T9:346, Thákurova 9, Praha 6 (see a guide and a map)
• Who: Pierre Donat-Bouillud
• Comment: This paper explores how developers use these type annotations, the type system semantics provided by type checking and inference tools, and the performance of these tools. It is interesting to see how a static type system can be retrofitted to a dynamic language without type annotations, how one type syntax can lead to 2 different type checking and inference rules (MyPy and PyType), and which type errors they catch. Useful when you want to add a type system to another dynamic language, R! The article is fairly easy to read; you can focus on the fist 2 sections or read the whole article.The article is from 2020 and the Python ecosystem, and in particular, type annotations, has grown a lot since: The evolution of type annotations in python: an empirical study has a large scale study of the evolution on more than 1 million commits from nearly 10 000 projects. Another famous article on Python and types is An Empirical Study of Type-Related Defects in Python Projects which compares issues from GitHub and type check results to assess how efficient type checking is a finding bugs, and finds that 15% of the defects could have been prevented by mypy.

• What: Code Style Sheets: CSS for Code by Sam Cohen and Ravi Chugh
• Paper: https://arxiv.org/pdf/2502.09386
• Where: Room S6 (2nd floor), Malostranské nám. 25 (see a map and a building plan)
• Who: Tomas Petricek
• Comment: The paper presents code style sheets - a system for nicely formatting source code that is inspired by CSS. The main technical challenge discussed in the paper is how to layout blocks of code that span over multiple lines. The paper is interesting as an example of research that is focused more on design than on theory or implementation, although it also comes with a small formalization of the core idea. It is also quite readable! Try to read sections 1-4 before coming to the meeting (and maybe have a quick look at illustrations in section 5 and 7).

• What: Capturing Types, by Aleksander Boruch-Gruszecki, Martin Odersky, Edward Lee, Ondřej Lhoták, and Jonathan Brachthäuser
• Paper: https://dl.acm.org/doi/pdf/10.1145/3618003
• Where: Room TH:A-1435, Thákurova 9, Praha 6 (see a guide and a map)
• Who: Filip Říha
• Comment: Capabilities are an alternative for denoting effects like mutability, exceptions or resource management. They are an alternative to the other popular methods, like checked exceptions or monads. The greatest benefit is it that capabilities can be expressed with plain arguments and handle polymorphism "for free". The paper describes a capture calculus, a type system that allows reasoning about scoped capabilities, even in presence of capturing closures and objects. For the meeting focus on sections 1 and 2, describing the overall idea of capturing types, and section 5 providing some more motivating examples. Sections 3 is the definition of the calculus, we can go through it at the meeting, but it would be good to be familiar with its syntax. A related talk about the current state of capabilities: Where Are We With Scala's Capabilities?, Martin Odersky.

• What: egg: Fast and extensible equality saturation by Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, Pavel Panchekha
• Paper: https://dl.acm.org/doi/pdf/10.1145/3434304
• Where: Room TH:A-951, Thákurova 9, Praha 6 (see a guide and a map)
• Who: Volodymyr Plita
• Comment: The paper introduces practical improvements to e-graphs—such as the rebuilding algorithm and e-class analyses—that make equality saturation efficient and extensible. The work made e-graphs popular again, and connects well-established theoretical ideas with a clean, usable implementation, supported by an open-source library that has been applied in multiple PL and optimization contexts for compilers. In the end I will also briefly mention slotted e-graphs that extend the original e-graph approach by adding first-class support for bound variables, allowing α-equivalent terms to be represented and rewritten uniformly. This makes equality saturation applicable and more efficient for languages and optimizations that involve binding, something traditional e-graphs and egg handle only awkwardly or inefficiently. The main parts to read are the introduction (section 1), then background of e-graphs (section 2) and sections 3 and 4 with the two core innovations.

• What: Sculpin: Direct-Manipulation Transformation of JSON by Horowitz, Hayatpur, Xia and Heer
• Paper: https://dl.acm.org/doi/10.1145/3746059.3747651
• Where: S204 (corridor in front of), Malostranské nám. 25 (see a map and a building plan)
• Who: Joel Jakubovic
• Comment: The paper presents a direct-manipulation environment for processing JSON data and building simple applications that have JSON as the back-end. The idea is that non-programmers can use the tool to complete tasks with JSON that would normally require programming. The paper is a nice implementation of the more general idea. The main parts to read are the sections describing Sculpin, i.e., Sections 3 and 4. It is useful to look at the related work (Section 2), fun to look at further examples (Section 5) and you can get an idea about HCI evaluation methods in Section 6.

• What: Practical compilation of fexprs using partial evaluation by Nathan Braswell, Sharjeel Khan, Santosh Pande
• Paper: https://arxiv.org/pdf/2303.12254
• Where: Room TH:A-951, Thákurova 9, Praha 6 (see a guide and a map)
• Who: Michal Žáček
• Comment: F-Expressions have historically been eschewed in favour of plain macros due to their inefficiencies and difficulties they pose for optimization. Since then, they have been forgotten and are missing from most all current languages. Nonetheless, they remain a fascinating subject due to their composability and the possibility of returning first-classness to our metaprogramming if their performance concerns are addressed. The article aims at showing that fexprs are a practical replacement of macros, and formulates a small purely functional fexpr based Lisp, Kraken, with an online partial evaluation and compilation framework that supports first-class, partially-static-data environments and can completely optimize away fexprs that are used and written in the style of macros. Focus on sections 1 and 2 for an overview. Read the intro of section 4 to get a taste of partial evaluation for fexprs.

• What: Restrictable Variants: A Simple and Practical Alternative to Extensible Variants
• Paper: https://drops.dagstuhl.de/storage/00lipics/lipics-vol263-ecoop2023/LIPIcs.ECOOP.2023.17/LIPIcs.ECOOP.2023.17.pdf
• Where: S204 (corridor in front of), Malostranské nám. 25 (see a map and a building plan)
• Who: Tomas Petricek
• Comment: Restrictable variants is an interesting language feature in the Flix programming language. It makes it possible to annotate algebraic data types (unions) to restrict what cases it can have, which is useful for example when writing a multi-pass compiler. The paper describes the feature and the theory behind it. For the meeting, focus on sections 1, 2, 5 and 6 - this provides a nice overview of the idea and the design space. Section 3 gets theoretical. Have a look and we can try to get through some of the formalism at the meeting!

• What: Introduction to the reading group, then No Silver Bullet -- Essence and Accident in Software Engineering -- by Frederick P. Brooks, then a surprise article...
• Paper: https://www.cs.unc.edu/techreports/86-020.pdf
• Where: Room TH:A-951, Thákurova 9, Praha 6 (see a guide and a map)
• Who: Pierre Donat-Bouillud, Filip Křikava
• Comment:

• What: Covariance and Controvariance: a fresh look at an old issue, Castagna
• Paper: https://www.irif.fr/~gc/papers/covcon-again.pdf
• Where: S8 (1st floor), Malostranské nám. 25 (see a map and a building plan)
• Who: Mickael Laurent
• Comment: The goal is to have a tutorial about set-theoretical types. The article is a good introduction to set-theoretic types, which focuses on implementation while most other works only give a mathematical definition. In particular, we may focus on section 4: Type algorithms for the language designer, which introduces the algorithm to decide subtyping using an interesting data structure (Binary Decision Diagram) that is used to represent logic formulas. A related article about set-theoretic types: https://www.irif.fr/~gc/papers/set-theoretic-types-2022.pdf.

• What: Deegen: A JIT-Capable VM Generator for Dynamic Languages
• Paper: https://arxiv.org/pdf/2411.10559
• Where: S204 (corridor in front of), Malostranské nám. 25 (see a map and a building plan)
• Who: Filip Křikava
• Comment: Building a high-performance JIT-capable VM for a dynamic language has traditionally required a tremendous amount of time, money, and expertise. The article presents Deegen, a meta-compiler that allows users to generate a high-performance JIT-capable VM for their own language at an engineering cost similar to writing a simple interpreter. Deegen takes in the execution semantics of the bytecodes implemented as C++ functions, and automatically generates a two-tier VM execution engine with a state-of-the-art interpreter, a state-of-the-art baseline JIT, and the tier-switching logic that connects them into a self-adaptive system. They implement LuaJIT Remake (LJR), a standard-compliant Lua 5.1 VM, using Deegen. Across 44 benchmarks, LJR's interpreter is on average 179% faster than the official PUC Lua interpreter, and 31% faster than LuaJIT's interpreter.

• What: Partial Evaluation, Whole-Program Compilation. Or, We have a Compiler at Home
• Paper: https://arxiv.org/pdf/2411.10559
• Where: Room T9:301, Thákurova 9, Praha 6 (see a guide and a map)
• Who: Pierre Donat-Bouillud
• Comment: The article shows a quick and effective way to get a compiler from an interpreter. This is an application of the 1st Futamura projection. However, this approach does not require a heavily specialized interpreter and can reuse a nearly unmodified interpreter body from an already existing one. They show 2 case studies for Javascript and Lua interpreters compiled to WASM. I recommend to skim the paper, at least looking at section 3 and one of the case studies.

• What: MyWebstrates: Webstrates as Local-first Software
• Paper: https://telecom-paris.hal.science/hal-04700748v1/file/klokmose24-uist.pdf
• Where: S204 (corridor in front of), Malostranské nám. 25 (see a map and a [building plan](https://cs.mff.cuni.cz/
• Who: Tomas Petricek
• Comment: Webstrates is a "computational medium" that makes it possible to create programs in a way that makes it easy to share them, modify them and collaborate around them. The paper presents an implementation of WebStrates that does not depend on a single server, but uses distributed peer-to-peer architecture based on the "local-first software" principles and is implemented based on the CRDT technology. This is a relatively light-weight paper that can be read as a whole. It is an interesting example of applying human-computer interaction research methods to a programming systems problem. I'd recommend skim-reading the whole paper - and reading parts that catch your attention in detail.

• What: The Design Principles of the Elixir Type System
• Paper: https://arxiv.org/pdf/2306.06391
• Where: Room T9:301, Thákurova 9, Praha 6 (see a guide and a map)
• Who: Thanks to Filip Říha for volunteering!
• Comment: This paper presents a new gradual type system for Elixir based on set-theoretic types. Elixir is a functional programming language based on the BEAM virtual machine (the VM of Erlang) used to build concurrent and fault-tolerant systems. A type system for this otherwise dynamic language aims to bring all of the static safety of types, not unlike what TypeScript is for JavaScript. However, unlike TypeScript, it is sound and does not introduce runtime checks in the code. Instead, it leverages type guards and pattern matches written by the programmer, a typical pattern in Elixir code. The paper is very practically oriented, showing why certain features were chosen for the type system and their usage, while it reserves very little space for formalization. I suggest reading section 2, an overview of the type system, and also section 3, which highlights some of the additions that the Elixir type system brings to the set-theoretical type theory (section 3.3 can be skipped, as it delves exhaustively into typing the Elixir records and maps).

• What: Stream Types
• Paper: https://dl.acm.org/doi/10.1145/3656434
• Where: Room S510 (5th floor), Malostranské nám. 25 (see a map and a building plan)
• Who: Thanks to Vít Šefl for volunteering!
• Comment: The paper presents a static type system for tracking information about streams of data in stream-based programming. It can capture "both complex temporal patterns and deterministic parallel processing". Streams are common data types in various reactive systems, user interfaces and signal processing, so it is interesting to see how to exactly capture what is going on! We will probably mostly focus on sections 1-3, so try to read those. It may be interesting to also talk about examples in section 5.2.

• What: Retrofitting effect handlers onto OCaml
• Paper: https://arxiv.org/pdf/2104.00250
• Where: Room T9:301, Thákurova 9, Praha 6 (see a guide and a map)
• Who: Thanks to Mickael Laurent for volunteering!
• Comment: The article describes an actual implementation of effects on a mainstream language, which did not support them before. The retrofitting approach is interesting in a PL design perspective: how do we evolve PL languages while maintaining backward and forward compatibility? Read at least sections 1-3 for the context and possibly the evaluation part (section 6). I will start by an introduction to algebraic effects.

• What: Reclaiming the Unexplored in Hybrid Visual Programming
• Paper: https://michael.homer.nz/Publications/Onward2024/ReclaimingUnexplored-Homer2024.pdf
• Where: Room S6 (2nd floor), Malostranské nám. 25 (see a map and a building plan)
• Who: Thanks to Joel Jakubovic for volunteering!
• Comment: The paper argues that we should do more work to explore visual representation of programs and visual programming. This is a short and readable paper and so I suggest looking at most of it in advance (sections 1-4). You can also experiment with the web-based demos available at: https://djel.org

• What: Syntax and Semantics of Dependent Types
• Paper: https://www.cs.uoregon.edu/research/summerschool/summer14/rwh_notes/ssdt.pdf
• Where: Room T9:364b, Thákurova 9, Praha 6 (see a guide and a map)
• Who: Thanks to Ondřej Kubánek for volunteering!
• Comment: This is a dense paper, but we can use it as a starting point for taking the next step towards making sense of dependent types! Ondřej volunteered to start with a 30 minute presentation, so this will be more of an introduction to the topic. It is still a good idea to look at sections 1 and 2 of the paper to know what to expect!

• What: Copy-and-patch compilation: a fast compilation algorithm for high-level languages and bytecode
• Paper: https://webspace.science.uu.nl/~swier004/publications/2023-icfp.pdf
• Where: S204 (corridor in front of), Malostranské nám. 25 (see a map and a building plan)
• Comment: A paper about an extremely fast compilation technique that produces good quality code (and is also used in Python 3.13!) The core ideas are described in sections 2, 3 and 4, so make sure to read those. We will likely also want to look at the evaluation results in section 5 and 6 (but you can skim the text there).

• What: Grokking the Sequent Calculus
• Paper: https://arxiv.org/pdf/2406.14719
• Where: Room T9:364b, Thákurova 9, Praha 6 (see a guide and a map)
• Who: Thanks to Maya Mückenschnabel for volunteering!
• Comment: A paper that presents the sequent calculus as a compilation target for "compiler hackers". This is written as a tutorial paper and it is probably best to read at least sections 1 and 2 in some details. For the rest, look at the first few paragraphs of each section to get a sense of what it's about.

• What: FP²: Fully in-Place Functional Programming
• Paper: https://webspace.science.uu.nl/~swier004/publications/2023-icfp.pdf
• Where: Room S510 (5th floor), Malostranské nám. 25 (see a map and a building plan)
• Who: Thanks to Jaromír Procházka for volunteering!
• Comment: The paper describes a subset of a functional langauge where programs can be executed without any memory allocation. Read section 1, which provides a nice overview of the language. We will certainly want to understand the calculus and well-formedness rules in section 2.1 and 2.2. It may be also interesting to look briefly at some of the algorithms in section 3 and 4.

• What: Type-Level Computations for Ruby Libraries
• Paper: https://arxiv.org/abs/1904.03521
• Where: Room T9:364b, Thákurova 9, Praha 6 (see a guide and a map)
• Who: Tomas Petricek, Pierre Donat-Bouillud
• Comment: An interesting perspective on what "types" can mean for dynamic programming languages. Read at least sections 2 and 3, which are accessible and provide nice overview. We can then try to read some of the formalism in section 4 or try to look at the evaluation in section 5. You do not need to read sections 4 and 5 in detail, but try to skim them to see what to find there!

• In previous years, the group was organised using a huge Google Doc (remarkably, nobody accidentally deleted it). Check it out for papers we've read in the past.
• Please share your paper ideas (and volunteer to present a paper) using Github Issues in this repository.