Published 02 Jul 2016. Tags: computer-science, formal-methods, oplss.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
(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