Harry R. Schwartz

I just spent two lovely/exhausting weeks in Eugene, OR at the Oregon Programming Languages Summer School (“OPLSS”). I had a great time, met some fine folks, and learned a bunch.

While there I kept a list of neat facts, papers, research groups, things to follow up on, observations, and things I was reminded of. I disavow any claim of expertise in any of these topics; most of them are things that sound interesting and that I’d like to dig into more deeply later. I’m publishing those here in no particular order.

If this seems like an absolute firehose of information then I’ve succeeded in modeling the OPLSS experience.

The OPLSS 2016 lectures are all online (or will be shortly).

Mark Jones’ Typing Haskell in Haskell* presents a formal description of Haskell’s type system by implementing a Haskell typechecker in Haskell.

The π-calculus is used for reasoning about concurrent computations.

OpenFlow: Enabling Innovation in Campus Networks, McKeown et al, SIGCOMM ‘08. The original paper on OpenFlow, a protocol for software-defined networking.

The standard SIGPLAN conferences (POPL, ICFP, PLDI, and SPLASH/OOPSLA) all host PLMW, the Programming Languages Mentoring Workshop, for undergrads and early grad students. It has some extra speakers and aims to provide a supportive environment.

Jon Sterling (now at CMU) has been working on RedPRL, a new NuPRL-inspired proof assistant.

Bob Constable tries to provide a gentle on-ramp into type theory with Naive Computational Type Theory.

Per Martin-Löf introduced a lot of ideas about intuitionistic type theory in Constructive Mathematics and Computer Programming.

Many of the contributions of NuPRL are discussed in Innovations in computational type theory using NuPRL.

The PLUM group at the University of Maryland has been doing some interesting work on extending Ruby’s type system for almost a decade.

The SAT/SMT/AR Summer School is a shorter and more focused annual workshop on solvers and automated logical reasoning. It moves around, but it was in Lisbon in 2016.

The Marktoberdorf Summer School is another two-week program, held annually outside of Munich.

Inferno DS is a port of Inferno (the successor to Plan 9) to the Nintendo DS.

I hadn’t thought of Google as doing much work in programming languages, but it sounds like there’s a pretty active group at the Aarhus office. They’re the folks that came up with Dart.

Ambrose Bonnaire-Sergeant (who maintains Typed Clojure, and just published a paper on it at ESOP ‘16) also maintains a repository of papers on dynamic typing.

I heard a nice piece of advice for anyone looking to go to grad school: try to publish a survey paper in your area of interest. You’ll have demonstrated your interest and diligence and you’ll have educated yourself on the state of the art in that area.

Awodey’s Category Theory is apparently an approachable-but-thorough introduction to the subject.

Some folks at OPLSS were a bit horrified at the idea of using Ruby. There are plenty of genuine problems with Ruby, for sure, and strong type systems have a bunch of advantages, but some of the problems they cited were a little funny to me (they were often very theoretical problems, but not issues that arise in practice). I especially liked, “but how do you know where anything’s defined?!”

Thumbnail Zoom is a Firefox plugin that enlarges image thumbnails when you hover over them. Very handy for important Reddit-related work.

Jacobs’ Categorical Logic and Type Theory examines type theory through the lens of fibrations.

I pronounce the Eq typeclass in Haskell as “eek” (as in “equal”), but some people apparently pronounce it as “eck.” So Eq a sounds a lot like the Latin ecce, which is sort of the equivalent of “achtung!” and can be a surprising/alarming thing to hear in a talk. I suspect that most people have less silly problems than I have.

Valiant and Brebner’s Universal Schemes for Parallel Communication introduced the Valiant load-balancing algorithm, which is used all over the place in distributed systems.

The Microtype LaTeX package subtly improves LaTeX typography in numerous ways.

Neelakantan Krishnaswami, who runs the Semantic Domain blog, wrote a great article on implementing abstract binding trees in OCaml (plus an addendum).

PLT Redex is a DSL (in Racket) for specifying and testing operational semantics. There’s also a book using it: Semantics Engineering with PLT Redex by Felleisen et al.

Valentin Antimirov’s Partial Derivatives of Regular Expressions and Finite Automata Constructions introduced the idea of taking the partial derivative of a regular expression, an idea which turns out to have all kinds of unlikely applications.

NSDI & SIGCOMM seem to be the two big conferences for software-defined networking.

Mike Hicks of the PLUM group at the University of Maryland publishes the PL Enthusiast blog.

Northeastern University hosts a series of monthly PL seminars that are, apparently, open to the general public.

Fully homomorphic encryption is a not-quite-extant-yet mechanism for performing arbitrary computation on encrypted data, which will be hugely important if a viable implementation can be found.

Matt Might wrote a terrific post on how to send and reply to email.

The Lean theorem prover is another new proof assistant.

Occurrence Typing Modulo Theories PLDI ‘16 by Kent et al. extends Typed Racket with dependent refinement types (e.g., an expression vec might by checked to satisfy (= (len vec) 3)).

Microsoft’s Z3 prover was open-sourced a few years ago and it’s since been widely used in academia.

I haven’t used it myself, but the Skim PDF reader seems to be very popular despite its age.

A rope is a data structure consisting of a binary tree with arrays for leaves. They’re commonly used to represent large blocks of text in editors.

Andrej Bauer maintains the PL Zoo, a collection of small languages written in OCaml that implement various interesting features.

Simon Thompson’s Type Theory and Functional Programming is out of print and a bit dated, but it’s available for free and apparently still a quality read.

The functional programming community calls a tree with a varying number of branches per node a “rose tree.”

Paul Levy has written up some great notes introducing the simply typed lambda calculus.

The Fields lectures on HoTT.

The lattice-style diagrams that everyone uses to illustrate partially-ordered sets are called Hasse diagrams.

Amal Ahmed gave an excellent series of lectures on verifying compilers this year. In previous years she covered some slightly different material; check her 2012 talks for a discussion of mutable references and the 2015 talks for free theorems.

Xavier Leroy’s paper on CompCert, Formal Certification of a Compiler Back-end POPL ‘06, was the first use of Coq to verify a real compiler (a C compiler, in this case), and laid the foundation for a lot of recent work in compiler verification.

Internet = Intergalactic Network.

Twelf is a logic programming language and proof assistant.

In his dissertation, A Theory of Typed Hygienic Macros, David Herman discusses a semantics for hygienic macro expansion. He also introduces the notion of binding signature types to specify the binding structure of macros.

Linear temporal logic is the logic associated with functional reactive programming (i.e., isomorphic to it, in the Curry-Howard sense).

Conor McBride’s The Derivative of a Regular Type is its Type of One-Hole Contexts extends the idea of derivatives to type theory and applies it in terms of zippers and holes. Erik Hinton also gave a great talk on this at Papers We Love NYC a couple of years ago.

Setting (set-input-method "TeX") in Emacs automatically inserts Unicode characters when typing the associated TeX. Very handy for taking mathy notes.

The functional logic programming language Curry lets you do crazy things like leveraging nondeterminism and running eval backwards with relatively familiar Haskell-esque syntax. The PAKCS implementation compiles to Prolog and seems pretty mature.

Ditzel & Patterson’s Retrospective on High-Level Computer Architecture examines the shortcomings inherent in machines with architectures designed to run “real” languages natively (e.g., the Lisp Machine).

Mininet is a tool for easily performing network simulation in a single VM.

In The Chemical Abstract Machine, POPL ‘90, Berry & Boudol model concurrent processes as molecules reacting in a beaker.

The deepest sympathy I can feel is looking over at the next speaker’s laptop screen and seeing that they’re desperately scanning man xrandr.