University of Minnesota Twin Cities PL Seminar

Things we've done in the past

  • Term Rewriting and All That
    • Baader and Nipkow 1998
    • An introduction to term rewriting systems.
    • Contains SML code
    • 11ch, 301pgs
  • The Rust Programming Language [Sep 2022 thru Dec 2022]
    • Klabnik and Nichols
    • Online book
    • 21ch
  • Seven Sketches in Compositionality [May 2021 thru Aug 2021]
    • Fong and Spivak 2019
    • Category theory book where the examples are gentler than other books we’ve tried
    • PDF
    • 7ch, 353pgs
  • The Art of Prolog [Sept 2020 thru April 2021]
    • Sterling and Shapiro 1994
    • A book starting at Prolog basics, and getting up to cool metaprogramming tricks, including Prolog interpreters in Prolog, compilers and planners, etc.
    • 24ch, 552pgs.
  • Logical Foundations [Jan 2020 thru July 2020]
    • Pierce et al Ongoing
    • The first of “the” Coq for PLT book series, Software Foundations
    • 17ch
  • Type Driven Development with Idris [Sep 2019 thru Jan 2020]
    • Brady 2017
    • An introduction to dependently typed programming in Idris.
    • 15ch, 480pgs
  • The Little Typer [July 2019 thru Sep 2019]
    • Friedman and Christiansen 2018
    • An introduction to dependent types with Pie.
    • 16ch, 242pgs
  • Category Theory in Context [May 2019 thru July 2019 (gave up…)]
    • Riehl 2016
    • The first category book we tried. It didn’t go well. (Written for mathematicians, not programmers!)
    • 6ch, 272pgs
  • Types and Programming Languages [Sep 2017 thru July 2018]
    • Pierce 2002
    • A very solid introduction to type systems for lambda calculi (including ones with object-oriented extensions) and programming language theory.
    • Introduces common notation used in PL papers very well.
    • This is probably worth doing every few years!
    • 32ch, 648pgs

Books we might want to read in the future

  • Abella: A System for Reasoning about Relational Specifications
    • Baelde, Chaudhuri, Gacek, Miller, Nadathur, Tiu, and Wang 2014
    • A tutorial for Abella.
    • I guess this is kinda a paper? It has chapters, so I’m putting it here.
    • 9ch, 89pgs.
  • Algebra of Programming
    • Bird and de Moor 1997
    • BMF/Squiggol
    • 10ch, 312pgs.
  • Call-by-Push-Value
    • Levy 2003
    • Favonia said I should read it ages ago and it’s been sitting it my TODO list ever since…
    • FAQ
    • 12ch, 381pgs.
  • Category Theory for Programmers
    • Milewski 2019
    • Site, PDF, Hardcover, Lectures
    • What it says on the tin
    • Covers more than Seven Sketches in Compositionality
    • Contains Haskell code
    • 31ch, 498pgs.
  • Formal Reasoning About Programs
    • Chlipala Ongoing
    • Coq book getting to the nice PL stuff sooner than SF
    • Open source! (CC and BSD)
    • 19ch, online (as of May 2021).
  • An Introduction to Array Programming in Klong
    • Holm 2018
    • Array programming as in APL, J, K, or Q.
    • Sample
    • 3ch, 100pgs.
  • Lisp in Small Pieces
    • Queinnec 1994
    • Essentially a series of tutorials on different ways to implement Lisp (and Scheme), and goes into some of the design decisions involved.
    • My introduction to continuations and denotational semantics.
    • 11ch, 514pgs.
  • Logic and Proof
    • Avigad, Lewis, and van Doorn 2017
    • The more mathy Lean book (the other is Theorem Proving in Lean, below).
    • 24ch, online.
  • Mathematical Components
    • Mahboubi and Tassi, Ongoing
    • Coq book teaching the Coq/SSReflect language, covering mostly math (rather than PLT)
    • Open source! (CC-BY-NC)
    • 8ch, 187pgs.
  • Object-Oriented Programming in Common Lisp
    • Keene 1988
    • An introduction to CLOS; if you think you know OOP and haven’t used CLOS, you should give it a try!
    • 12ch, 288pgs.
  • Optics By Example
    • Penner 2020
    • Lenses, Prisms, etc. in Haskell
    • 20ch, 420pgs.
  • Partial Evaluation and Automatic Program Generation
    • Jones, Gomard, and Sestoft 1999
    • What it says on the tin.
    • Implements very cool programs in surprisingly little code.
    • 18ch, 425pgs.
  • Pharo by Example
    • Various, Ongoing
    • Open source! (CC-BY-SA)
    • PDF
    • 17ch, 312pgs (as of May 2021).
  • Practical Foundations for Programming Languages
    • Harper 2016
    • Seems TAPL-shaped?
    • 18ch, 580pgs.
  • Principles of Program Analysis
    • Nielson, Nielson, and Hankin 2005 (2nd printing)
    • Covers control flow and data flow analyses, and abstract interpretation.
    • Might be fun to implement along with the book.
    • 6ch, 452pgs.
  • Program Design by Calculation
    • Oliveira 2021/Ongoing
    • BMF/Squiggol book, allegedly better presentation than Algebra of Programming, but still a draft
    • Being continuously updated
    • Lots of material covered in Eric’s Spring 2021 CSCI8980, so we might wanna hold off until it’s out of people’s recent memory.
    • PDF
    • 10ch, 313pgs (as of Feb 2021).
  • Program Logics for Certified Compilers
    • Appel 2014
    • Separation logic, from the CompCert people
    • Sample
    • 46ch, 472pgs.
  • Programming with Higher-Order Logic
    • Miller and Nadathur 2012
    • The λProlog book
    • 11ch, 320pgs.
  • The Reasoned Schemer
    • Friedman, Byrd, and Kiselyov 2005 (1st ed)
    • MiniKanren. Easier to implement than Prolog, not depth-first-search-by-default.
    • Written as a dialogue.
    • If we do this, there’s a bunch of really cool miniKanren papers I’d like after, including a couple neat program-synthesis things.
    • 12ch, 169pgs.
  • Software Abstractions
    • Jackson 2011
    • The Alloy tutorial; this talk sold me on this being really cool.
    • 6ch, 376pgs.
  • The TeXbook
    • Knuth 1984
    • 27ch, 496pgs.
  • Theorem Proving in Lean
    • Avigad, de Moura, and Kong 2017
    • The more CSy Lean book (the other is Logic and Proof, above).
    • 11ch, online.
  • Warren’s Abstract Machine: A Tutorial Reconstruction
    • Aït-Kaci 1991
    • A more readable version of An Abstract Prolog Instruction Set, essentially.
    • However, last time I tried to read it, I found enough errata that it’s not as directly useful as an implementation guide as it could be.
    • Still, good for the 10,000-foot view.
    • 6ch, 114pgs.

Papers we might want to read in the future

  • An Abstract Prolog Instruction Set
    • Warren 1983
    • Initial presentation of the Warren Abstract Machine; I’ve been warned this is less than completely clear, but never read it.
    • 34pgs, so maybe avoid or split up.
  • An Algorithm for Optimal Lambda Calculus Reduction
    • Lamping 1990
    • Initial presentation of interaction nets, I think?
    • 16pgs, 4 of which are pictures.
  • Build systems a la carte: theory and practice
    • Mokhov 2020
    • Compares build systems and breaks them down into components, then prototypes new ones from the components
    • Covers Make, Excel, Shake, and Bazel
    • Revised + expanded version of original “Build systems a la carte” (Mokhov 2018)
  • Call-by-Value is Dual to Call-by-Name
    • Wadler 2003
    • 13pgs.
  • Clowns to the Left of me, Jokers to the Right
    • McBride 2008
    • A generalization of zippers to allow representing a computation in progress.
  • Functional Pearl: Data types a la carte
    • Sweirstra 2008
    • Recursion schemes-like machinery for extensible types.
    • 14pgs.
  • The Gentle Art of Levitation
    • Chapman 2010
    • Datatypes, including induction, without needing a special declaration type or anything. (Stahl is doing a variation of this, for which induction is sadly trickier…)
    • 12 pgs.
  • Ghosts of Departed Proofs (Functional Pearl)
    • Noonan 2018
    • Proof-checked code in Haskell with a tasteful set of extensions (i.e., not like this).
  • Hoopl: A Modular, Reusable Library for Dataflow Analysis and Tranformation
    • Ramsey 2010
    • What it says on the tin.
    • 16 pgs.
  • Monad Transformers and Modular Algebraic Effects: What Binds Them Together
    • Schrijvers 2019
    • Random algebraic effects paper.
    • 17pgs, 2 of which are cover pages, 3 of which are appendices.
  • Quick Compilers Using Peephole Optimization
    • Davidson 1989
    • Turns out peephole optimization has a really really high payoff vs effort to implement (as the only optimization the compiler does, at least).
    • 22 pgs, 5 of which are appendices and some chunk of which is describing a quite cursed pattern matching engine. (This is from before computers were fast, so I suppose seding the assembly was too slow?)
  • Selective Applicative Functors
    • Mokhov 2019
    • An extension of applicative functors to add choice, which lets them replace monads in some circumstances.
    • 29 pgs.
  • Sequent Calculus as a Compiler Intermediate Language
    • Downen 2016
    • What it says on the tin, as a replacement for GHC Core.
    • 15 pgs.
  • A tutorial implementation of dynamic pattern unification
    • Gundry 2012
    • A tutorial of implementing metavariables in a dependently-typed language.
    • Contains Haskell code
    • Yeah, this one’s transparently from my “to read” bucket.
  • There is no Fork: an Abstraction for Efficient, Concurrent, and Concise Data Access
    • Marlow 2014
    • Smarter IO behavior when IO is done in applicatives (which don’t include ordering).
    • 13 pgs.
  • A Unified Approach to Solving Seven Programming Problems (functional pearl)
    • Byrd, Ballantyne, Rosenblatt, and Might 2017
    • Some really cool code synthesis stuff in miniKanren
    • 26pgs.
  • Yacc is Dead
    • Might 2010
    • A parsing algorithm using Brzozowski derivatives, much easier to implement than LALR (comparable to a middling-efficiency regex engine, iirc).
    • We might’ve already done this a couple years ago, but I don’t remember.
    • 18pgs.

Other resources

  • Nathan Ringo runs a Forth workshop
    • Probably something like, 2-3 weeks on learning the language, 1 week on a “metacircular” implementation, 1 week on bootstrapping, 2-3 weeks on advanced topics
  • OPLSS 2015 - Logical Relations
    • Video lectures about proving “difficult to prove” properties, e.g. strong normalization of STLC
    • Info Site
    • Videos