7. Reading Project

7.1. Overview

In this final project, you are going to get a taste of some cutting-edge research in programming language design and implementation. Specifically, you’ll get to read some selected seminal and recent manuscripts, covering various aspects of PLDI that we touched upon in the class: low-level languages, interpreters, parsing, types, and optimisations.

You will be required to choose one paper from the list below (each paper can be chosen by at most one student) and submit an essay that summarises the paper’s key ideas, technical contributions, and also provides its evaluation. Unlike previous projects, this final task for PLDI will not require you to implement a part of a compiler. However, you sitill might have to write some code, sometimes in languages you’ve never programmed in before.


Please, set aside a good amount of time for this project, as it’s not meant to be done in a single evening and requires reflection on the research ideas, most of which will be new for you.

7.1.1. The Task

The list of the papers below is a mix of classical and modern results in programming languages and compilers, and, you will have to submit a report summarising the key ideas and contributions of one paper. A typical report is expected to be 3-5 pages. The full grade for this project is 10 points, making it 10% of your final score for the module. The grade will be assembled from the following aspects that have to be present in your report.

1. Motivation and Background [3 points] You should clearly articulate the answers to the following questions about the paper you’ve read:

  • What is the problem that the paper solves?
  • Why is it important?
  • What were the existing approaches to address this problem (if any), an why they were found unsatisfactory by the authors?

2. Key Ideas and Contributions [3 points] Please, explain the following aspects of the paper.

  • What is the main methodology for solving the problem?
  • What are the challenges for implementing the solution?
  • Try to relate the ideas from the paper to the concepts explained in this class as you understand them. How are they extending what we have discussed in the lectures?

When explaining the technical ideas, do not paraphrase the text from the paper, use your own words. Also, unless absolutely crucial, avoid copying formulas/plots from the paper. If necessary, produce your own, as described in the next item.

3. Evaluation [4 points] This is the most important part of your report, in which you need to show a good understanding of the paper’s ideas. This can be done by implementing at least one of the points from the following list (you don’t have to do all of them, just one would suffice).

  • If the paper describes a tool (such papers will be marked with [T]), show an example run of the tool and outline your own experience of using it. This will require figuring out how to install and use the tool. For your demonstration, if possible, please, avoid using the same examples as in the paper, or at least modify them in a meaningful way.
  • If the paper describes a conceptual approach for addressing a problem, e.g., an algorithm or a typing discipline (such papers are marked with [A]), present a paper-and-pencil development of an example showing the algorithm/approach in action. The example must not be taken directly from the paper.
  • For some foundational papers that describe seminal theoretical ideas and are typically published more than 10 years ago (such papers are marked with [I]), provide a survey of the later work that has built on those ideas. Consider using Google Scholar for this. You don’t have to go through the entire body of the follow-up work (some papers have hundreds of citations by now); pick what you consider good examples of how the idea is used in practice nowadays or how it has been implemented in the approaches that came later. Your survey will be stronger if you also pinpoint the shortcomings of the original idea that have been addressed in later works.

Some of the papers will make it possible to provide evaluation on more than one point from the list above. While it’s not required to get the full score, feel free to do so—I’ll be even more delighted to read your report.


Some papers fall into more than one category. You are at freedom to select an appropriate mode of evaluation for them; the letter marks (A, T, and I) should be treated only as a suggestion. Several papers from the list below might not articulate very clearly the problem they are solving or the contributions, and just describe a system. For those papers (marked [S] in addition to [T]), the stress is going to be on evaluation, which will be judged out of 6 points, while the descriptions of the background and contributions can be short and will be graded out of 2 points max each.

The structure of your report does not have to follow verbatim the parts described above. Feel free to add your own writing with reflections on research in PL, outline your journey into the topic of your paper, and add a conclusion

7.1.2. List of Papers

The papers in the list below are grouped according to their sub-area within PLDI research field. Make sure to indicate your choice of the paper in a Google spreadsheet. Please, do it ASAP, otherwise your preferred paper might be taken by someone else.


You may change your selected paper until the final deadline. You may also swap papers with someone else by changing your preferences in the shared spreadsheet.

Low-Level and Intermediate-Level Languages

  1. Bringing the Web up to Speed with WebAssembly [T]. Haas et al., PLDI 2017. Evaluating this paper will require you to learn how to read and write programs in wasm.
  2. Typed Assembly Language [A,I]. Greg Morrisett, in Advanced Topics in Types and Programming Languages. Chapter 4, 2005. This is a chapter in an advanced textbook, which is not available online. Check out the linked article and get in touch with me for a copy.
  3. Formalizing the LLVM Intermediate Representation for Verified Program Transformations [T,S]. Zhao et al., POPL 2012. This paper describes a substantial Coq development so it will build, to some extent, on the FPP setup. For your evaluation, try install it and run the code artefacts, or at least explain some of the theorems from the Coq code.

Interpreters and Program Transformations

  1. Run Your Research: On the Effectiveness of Lightweight Mechanization [T]. Klein et al., POPL 2012. To evaluate this paper, you might want to learn how to use the PLT Redex tool.
  2. Defunctionalization at Work [I,A,T]. Danvy and Nielsen, PPDP 2001.

Lexing and Parsing

  1. Regular-Expression Derivatives Reexamined [I,A]. Owens et al., 2009. This paper presents an algorithm for defining automata for regex matching using the idea of Brzozowski derivatives.
  2. Parser Combinators in Scala [T,S]. Moors et al, 2008. This paper is essentially a description of a Scala library. You will be expected to show a good demo for your evaluation. You are encouraged to consult some foundational papers explaining the combinator approach to parsing.
  3. Parsimony: An IDE for Example-Guided Synthesis of Lexers and Parsers [T]. Leung and Lerner, ASE 2017. Evaluating this paper will require you to master the usage of an interactive tool for generating lexers and parsers.
  4. Parsing with Zippers (Functional Pearl) [A,T]. Darragh and Adams, ICFP 2020. This paper comes with an OCaml implementation, which you can find and use for your evaluation.

Types and Type Systems

  1. Featherweight Java: A Minimal Core Calculus for Java and GJ [A,I]. Igarashi et al., OOPSLA 1997.
  2. Gradual Typing for Functional Languages [A,I]. Jeremy Siek, Scheme Workshop 2006.
  3. Contracts for Higher-Order Functions [A,I]. Findler and Felleisen, ICFP 2002. You might want to check the Racket programming language for the implementation of the ideas from the paper.
  4. Refinement Types for Haskell [T,S]. Vazou et al., ICFP 2014. For evaluating this paper, you might want to check Liquid Haskell Tutorial. You will also need to install Haskell, obviously.
  5. Java and Scala’s Type Systems are Unsound: The Existential Crisis of Null Pointers [A,T]. Amin and Tate, OOPSLA 2016. For your evaluation, you might want to construct a few new examples, following the ideas from the paper.
  6. Type Systems as Macros [T]. Chang et al., POPL 2017. You will need to install Racket for your evaluation.
  7. Practical Pluggable Types for Java [T], Ernst et al. ISSTA 2008. You will need to install the Checker Framework for your demo.
  8. Dynamic Witnesses for Static Type Errors [A,I], Seidel et al. ICFP 2016. As the tool for this paper might be difficult to run (as it has no documentation), you are expected to explain how the underlying algorithm works. You are also encouraged to get in touch with the authors for extra instructions.

Code Analysis and Optimisations

  1. Introduction to Abstract Interpretation [I, A]. Bruno Blanchet, 2002.
  2. Higher-Order Control-Flow Analysis [I,A]. Matt Might, PhD Thesis, 2007. You only need to read Chapters 1–5 of Might’s thesis.
  3. Flow-Directed Closure Conversion for Typed Languages [A,T]. Cejtin et al., ESOP 2000. Make sure to explain what is flow analysis, and what is closure conversion (feel free to check other sources for it). For your evaluation, you can either implement the closure analysis for a small subset of source and target language (this would be really cool!), or demonstrate how it works on an example, different from the one from the paper.
  4. Modular, Higher-Order Cardinality Analysis in Theory and Practice [A,T] Sergey et al., POPL 2014. You will need to install Haskell to evaluate this paper. Also, check instructions on how to dump Haskell “Core” IR with the analysis-inferred annotations.
  5. Equality Saturation: A New Approach to Optimization [I], Tate et al., POPL 2009. You might also want to check this page for additional materials.
  6. EigenCFA: Accelerating Flow Analysis with GPUs [I], Prabhu et al., POPL 2011.
  7. Provably Correct Peephole Optimizations with Alive [I,T], Lopes et al., PLDI 2015.

Compilation Strategies

  1. The Essence of Compiling with Continuations [I]. Flanagan et al., PLDI 1993. Your report should include examples of CPS transformation.
  2. Space-Efficient Closure Representations [I], Shao and Appel, LFP 1994. Make sure to work out a number of examples for your explanation.

Verified Compilers

  1. Formal certification of a compiler back-end or: programming a compiler with a proof assistant [I,T], Xavier Leroy, POPL 2006. Ideally, you should be able to compile CompCert and run it, comparing to, e.g., gcc in terms of performance and available features. For your survey, make sure to cover some of the follow-up works.
  2. CakeML: A Verified Implementation of ML [T,I], Kumar et al., POPL 2014. Ideally, you should be able to compile CakeML and run it, reporting on your observations and comparing it with a Standard ML compiler. For your survey, make sure to cover some of the follow-up works.


  1. How to Make Ad-Hoc Polymorphism Less Ad Hoc [I,T]. Wadler and Blott, POPL 1989. For your evaluation, you are expected to install Haskell and show how these ideas are used there.
  2. Ott: Effective Tool Support for the Working Semanticist [T]. Sewell et al., ICFP 2007. Your report will have to be typeset in LaTeX and feature Ott-generated snippets.
  3. Synthesis Modulo Recursive Functions [I,T]. Kneuss et al., OOPSLA 2015. It is recommended to base your evaluation on trying different examples with Leon synthesis tool.
  4. Effect-Driven QuickChecking of Compilers [T]. Midtgaard et al., ICFP 2017. To understand the main toolset for this work, make sure to read on the QuickCheck tool for property-based testing and check the examples of its use in Haskell, Scala and OCaml.

7.1.3. Tips and Hints

  • Don’t worry if you don’t understand all technical details in the paper upon the first read. Most of the papers require several readings for getting a good idea on what is going on there.
  • On your first read, go over the abstract, intro, overview and the evaluation/experiments sections of a paper, ignoring its middle technical part. Once comfortable with those, read the technical details. Here is some good advice on reading research papers.
  • If possible, try work out examples from the paper by yourself, once you think you understand the main idea.
  • While it is not strictly required, you might need to work with additional resources when reading the paper. Don’t be afraid to look up on the internet for the tutorials, blog posts, and repositories, which might elaborate on the technical details of your paper and provide additional examples.
  • It is also okay to not fully understand some intricacies of the paper’s development. Due to space constraints papers frequently omit many details, which you probably don’t need for your report and evaluation anyway.
  • If you feel brave, you can try to reach out to the authors of the papers for explanations—it is perfectly acceptable to do so, especially for recently published works. If you are not sure how to contact them, let me know. Do so well before the deadline, as personal communication takes time.
  • Most importantly, try to make the best out of this project by getting familiarised with the ideas of the paper you have chosen. All of the selected papers represent either cutting-edge research in PLDI or some well-established techniques, and those ideas might come handy at some point in your future career in software development.

Good luck!