david's pl notes

David's PL Notes

Sep 02, 202413 min read

About this website

Welcome to David’s PL Notes! This website contains a bunch of notes on topics on programming language (PL) implementation and theory. This site might be useful for you for a few reasons:

  • You’re currently studying for the UC Berkeley PL Prelim, and you’re looking for topics to study, resources for those topics, and general notes on the relevant topics.
  • You’re interested in PL generally, and are looking for readings & notes on a survey of different PL-related topics.

In either case, this site has a bunch of resources that might be helpful for you! Specifically, we have:

  • A syllabus (see below) of different topics and readings that cover a broad range of PL topics.
  • Reading notes on individual readings with respect to these topics.
  • Topic notes that synthesize multiple (some of the reading notes do this as well)
  • Study guides that summarize all of the different topics mentioned here (good as a guided index into the rest of the notes).

I originally wrote these notes in preparation for the Berkeley PL Prelim, so they’re provided as-is; I basically haven’t changed them since I copy-pasted them here, so a lot of them might make reference to Prelim-related things.

If you have any questions, feel free to email me (it’s on my website linked above).

Formatting caveats

As a consequence of me manually copy-pasting my notes to this site, there might be missing pages; this is unintentional, and you should let me know if you run into this!

Additionally, type judgments/derivations will look weird---they’re missing the horizontal line dividing consequence and consequent, because of LaTeX rendering weirdness with the static site generator I’m using. They’ll look like this:

Apologies in advance :^)

If you’re taking the PL prelim, there are a number of things to keep in mind. The syllabus suggests that, even though it lists a bunch of different topics and readings for those topics, those alone won’t be sufficient to cover the material needed:

Keep in mind that some topics---for example language design and implementation---are rather broad. It is expected that students can answer reasonable open-ended questions that go beyond the content of papers listed below.

But don’t let this intimidate you! For the most part, the PL prelim isn’t designed around memorization of specific vocabulary or parts of specific papers; rather, it’s about understanding and internalization of concepts. So while the reading serves as a useful resource and starting point to ground your understanding in each of the topics, you’ll probably find yourself naturally looking for other resources to help supplement your understanding of the topics!

As for how you can find these other resources, the short answer is: Google! A lot of the topics have extensive Wikipedia pages, along with lecture slides and notes from other folks who have helpfully uploaded their course materials online. When I studied for the test, a lot of how I acquired these extra bits of information was through these other auxiliary resources: lecture notes, StackOverflow answers, that sort of thing. I also used notes from other folks who had taken the PL prelim beforehand (see the extra resources in the section below this). If you’re looking for pointers to what kinds of readings are helpful for building understanding, all of the resources I used for each reading or topic are linked within the notes for those readings/topics, respectively. But this proecss will necessarily look different for everyone, and the readings that work for me might not necessarily work for you!

In general, these notes are meant to be a supplement, helpfully summarizing and explaining concepts that might have more dense explanations in other readings. Most of the studying and learning you’ll do is in taking your own notes though: internalizing and building intuition for these concepts yourself!

To give you an idea of how much reading and studying I did leading up to this test, the topics/readings listed below have checkboxes according to this legend:

  • Uncomplete reading or topic
  • Completed (or skimmed) reading or topic
  • Missing reading
  • % Optional reading (prepended with a %)

If you’d like to follow along with my study schedule, here’s the order I went in:

  • First, I created the scheduled study notes, corresponding to the PL Prelim Study schedule provided by past students.
  • Next, I created extra topic notes for topics that weren’t covered by this scheduled study.
  • Finally, I created study guides in the week before the test to go over my old notes and figure out the key ideas to retain.

Extra resources

This folder from Manish contains past resources, including the CS 164 course reader, past schedules, past notes, and textbook PDFs.

These links also have some more readings if needed:

Scheduled study

Study guides

One-page (ish) summaries of all the topics.

Extra topics

Extra notes on topics that weren’t explicitly scheduled, or that aren’t explicitly mentioned in the syllabus but are things we’re expected (?) to know.

Syllabus

Languages

Goal

Know syntax, major features, and implementations of these languages. Be able to critique features (see Topics/features to know) and program and give examples in several of these languages.

  • C
  • C++ (classes, inheritance, templates)
  • Java (reflection, generics)
  • Python, Ruby
  • Prolog and Datalog
  • ML (type inference)
  • Scheme (continuations, dynamic typing, macros)

The art of language design

Lightweight intro to (complexity of) PL design, broad motivating ideas behind (and critiques of various langs.

Additional language design notes from Sarah’s 294

Topics/features to know

Semantics & types

Readings

3 TAPL chapters ~ 1 paper; do memos accordingly

Optional

  • % Girard, LaFont, and Taylor’s Proofs and Types chapters 2-7 are a remarkably compact presentation of the basic proof theory that makes types work.
  • % Frank Pfenning’s Computation and Deduction covers similar ground, but in much greater detail. His webpage has a number of exceptionally readable papers on computational logic.
  • % The explanation of denotational semantics in John C. Mitchell’s Foundations for Programming Languages is extremely clear and comprehensible.  If you find Winskel to be frustrating, try this.

Implementation, program analysis, & optimization

See Dragon Book for general readings. See also discussion on HN about it for alternatives.

Basics

Extra topics

Static analysis

Extra

Algorithmic verification, testing, and debugging

Optional

  • % C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, R. Stata Extended Static Checking for Java Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation (PLDI 2002) Tool publicly available at http://research.compaq.com/SRC/esc/
  • % S. Malik and L. Zhang, Boolean Satisfiability: From Theoretical Hardness to Practical Success, Communications of the ACM, vol. 52, no. 8, August 2009.
  • % E.A. Lee and S. Seshia, Introduction to Embedded Systems, A Cyber-Physical Systems Approach, 2nd Edition. Chaps. 13 and 15. http://LeeSeshia.org.
  • % Clarke, Grumberg, and Peled. Model Checking (MIT press). Chapters: 1. Introduction, 2. Modeling Systems, 3. Temporal Logics, and 4. Model Checking
  • % Symbolic model checking: 10^20 States and beyond. J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, L.J. Hwang, Information and Computation, Volume 98, Issue 2, June 1992, Pages 142-170, ISSN 0890-5401.http://www.sciencedirect.com/science/article/B6WGK-4DX44C6-6T/2/fe89ddab72b8634621ce5d293f3a8660
  • % A machine program for theorem-proving (DPLL paper). Martin Davis, George Logemann, and Donald Loveland. 1962. Commun. ACM 5, 7 (July 1962), 394-397. http://doi.acm.org/10.1145/368273.368557
  • % Chapters on constraint-solving based, and type/effect systems found in Nielson et al.’s Principles of Program Analysis http://www.amazon.com/Principles-Program-Analysis-Flemming-Nielson/dp/3540654100
  • % Greg Nelson: Techniques for Program Verification.Ph.D. Thesis. 1980.
  • % Randal E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, Vol. C-35, No. 8, August, 1986, pp. 677-691
  • % Manuvir Das, Sorin Lerner and Mark Seigle. ESP: Path-Sensitive Program Verification in Polynomial Time. PLDI 2002.
  • % Something on abstraction (say one of the early SLAM/Blast papers or Graf-Saidi).
  • % Static checking of assertions/annotations, maybe ESC/Java paper (Extended static checking for Java, Flanagan, et al., PLDI 2002)
  • % Specification inference, invariant generation, eg DAIKON.

Mock prelims

Random with Justin

Targeted with Justin

Parker one-off

Federico one-off

Graph View

Backlinks

  • No backlinks found