Resources
Catching up with Programming Languages (CS152)
-
See the CS152 schedule for lecture notes. Particularly relevant are lectures 2-5 on semantics, lecture 7 on lambda calculus, lecture 11 on simply-typed lambda calculus (STLC).
-
See the CS152 resources for book recommendations and programming language pointers.
Finding papers
Venues
The main conferences in programming languages are:
They are now all part of the same journal, Proceedings of the ACM on Programming Languages (PACMPL).
Other journals in programming languages include HOSC, JFP and TOPLAS.
Other conferences in programming languages include ECOOP, FLOPS, GPCE, ITP.
Workshops co-located with conferences above can also be good source of papers. Workshops include PEPM, PADL, language-specific workshops (Scheme, miniKanren, Haskell, Coq, …), topic workshops (egraphs, …), and many more. Note that for students, PLMW workshops co-located with the main conferences provide funding and mentoring.
Some topics/papers
LLMs/PL interplay
- ICLR’22: Co-training for Theorem Proving with LLMs (PDF),
- OOPSLA’22: Specification-Guided Component-Based Synthesis for Effective Libraries (link),
- OOPSLA’24: Statically Contextualizing Large Language Models with Typed Holes (link).
- COLM’24: An In-Context Learning Agent for Formal Theorem-Proving (link).
- NeurIPS’23: LeanDojo: Theorem Proving with Retrieval-Augmented Language Models (link).
- NeuRIPS’24: Grammar-Aligned Decoding (link).
- Guy Van den Broeck, Prof at UCLA, has some papers around controlling LLMs: Ctrl-G, GeLaTo, Semantic Probabilistic Layer.
- Gabriel Poesia, PhD student at Stanford, has some papers around LLMs for mathematical discovery, e.g., NeurIPS’24: Learning Formal Mathematics From Intrinsic Motivation (paper, code).
Reflective Towers of Interpreters
Prof. Nada Amin might present on reflective towers of interpreters, and their collapsing using the following sequence of artifacts/papers:
- 3-LISP,
- Brown (non-tower & tower),
- Blond (primer and paper),
- Black (scheme and metaocaml),
- Pink and Purple (POPL’18).
As a staring point, see the SIGPLAN blogpost on reflective towers by Prof. Nada Amin.
Algebraic Effects
Tutorials
- “An Introduction to Algebraic Effects and Handlers” by Matija Pretnar
- “Handlers in Action” by Ohad Kammar, Sam Lindley and Nicolas Oury
Theoretical Foundations
- “What’s Algebraic about Algebraic Effects and Handlers?” by Andrej Bauer: Good starting paper for those not intimately familiar with category theory and abstract algebra
- “Semantics for Algebraic Operations” by Gordon Plotkin and John Power: Original Paper on Algebraic Effects
- “Handlers of Algebraic Effects” by Gordon Plotkin and Matija Pretnar: Original Paper on Handlers for Algebraic Effects
- “Combining Effects: Sum and Tensor” by Martin Hyland, Gordon Plotkin and John Power
Applied Systems
- “Algebraic Effects, Fibers, Coroutines Oh My!” by Brandon Dali: Describes Hooks and Fibers for React as Algebraic Effects and Coroutines
- Poutine: A Guide to Programming with Effect Handlers in Pyro: This describes Pyro’s current effect handler stack, Poutine
- “Effective Concurrency with Algebraic Effects” by KC Sivaramakrishnan
Misc
- A bibliography maintained by Yallop
- “Generalized Evidence Passing for Effect Handlers (or, Efficient Compilation of Effect Handlers to C)” by Xie and Leijen
Binding Structures
- The POPLmark Challenge
- A Solution to the PoplMark Challenge using de Bruijn indices in Isabelle/HOL
- DBLib: a Coq library for working with de Bruijn indices
- DeBruijn: Intrinsically-typed de Bruijn representation
- A locally nameless solution to the POPLmark challenge
- Locally Nameless at Scale
- The Locally Nameless Representation
- Higher-Order Abstract Syntax
- Boxes Go Bananas: Encoding Higher-Order Abstract Syntax with Parametric Polymorphism
- Parametric Higher-Order Abstract Syntax for Mechanized Semantics
- Formal Metatheory of Second-Order Abstract Syntax
- Nominal Logic: A First Order Theory of Names and Binding