OPLSS Flotsam

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

.