# University of Minnesota Twin Cities PL Seminar

## Books

This page has things, TODO

## 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
- 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)
- 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.
- 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

- Term
*Re*writing and*All That*- Baader and Nipkow 1998
- An introduction to term rewriting systems.
- Contains SML code
- 11ch, 301pgs

- 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.

- The Rust Programming Language
- Klabnik, Nichols, Various 2019/Ongoing
- The standard book
- Open source, paper version here
- 20ch, online (as of May 2021).

- 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, looks like.
- 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
`sed`

ing 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.

## Things that are neither books nor papers

- Nathan 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

## Things we've done in the past

- 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
- 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