POPL 2017

Some things I learned by attending POPL talks.

Learning from Interpretations

The LFI-Problog algorithm, for doing inference on probabilistic logic programs.

Finding Counterexamples from Parsing Conflicts

How the CUP parser generator explains conflicts.

Verdi

A system for implementing and verifying distributed algorithms.

Push/Pull for Transactions

A unified model for understanding many transactional systems.

Tree Buffers

Circular buffers are one of the most fundamental and pervasive data structures. They are an efficient implementation for buffering linear sequences. Tree buffers are a more general data structure.

RIP Herman Conjecture (2005-2015)

In 1990, Herman proposed a sweet self-stabilizing protocol. In 2005, McIver and Morgan conjectured that its running time is $\frac{4}{27} N^2$. Well … they were right.

Why Do We Fail?

What is there to do if a problem refuses to be knocked down? There's a generic problem solving strategy for that.

Watching Horn

How to use watched literals (or, rather, vertices) to do breadth-first search in Horn hyperdigraphs.

At Most R

How to encode a cardinality constraint as boolean constraints.

Minimizing Weighted Automata via Linear Algebra

In this post I present the minimization problem for weighted automata, closely following a paper by Stefan Kiefer and Björn Wachter. I do add lots of steps that aren't necessary. To me, they make the result look less like magic. I really like the mixture of automata and linear algebra.

Minimal Sets over Monotone Predicates

This post describes a very nice use of binary search. I learned about it from a paper by Joao Marques-Silva, Mikolas Janota, and Anton Belov.

Datalog and MaxSat: an Unexpected Match

In which I tell you how I got a bottle of Scotch.

PLDI 2014 — Compiler Validation via Equivalence Modulo Inputs

The title is stolen from a paper that was presented at PLDI. I did not see the presentation, so this summary is based on looking at the paper.

PLDI 2014 — Presentations I've Seen

These are tiny summaries of some of the talks from PLDI 2014.

Program Analysis, from 2000 to 2009

Very extremely roughly, static program analysis is the area concerned with looking at the text of computer programs and deciding based on that whether they are crap or not. There is, of course, a very easy way to write a sound program analyzer. In Python3 it would look like this: print('crap'). It's sound because it never lets bad programs go without calling them out. But you often want something a bit more friendly (aka complete, aka precise). Being precise is difficult, and that's why this is still an area of active research. Here are few papers from the decade 2000–2009 that are influential, and pointers to associated tools.

Some Talks from POPL 2014

These are my notes from some of the most memorable talks at POPL. What I found memorable is heavily biased. First, I attended less than half of the talks. (More than half is physically impossible.) Second, I did not read the papers. Third, I found some presentations memorable because their content matched my background, and others because of the presentation style. Fourth, it's likely I payed more attention to talks given by people I know.

Awards and Invited Talks at POPL 2014

These are my notes from attending presentations at POPL and associated events. This post is about the non-regular talks I attended.

Certificates and Simplifications for Quantified Boolean Formulas

It starts poetically, with a story involving parallel universes, and ends prosaically, with a link to a paper to appear in LPAR 2013.

Squaregraphs

On Tuesday, Donald Knuth gave a talk about squaregraphs. I'm summarizing here what I learned, and I'm including the open problems that Knuth mentioned.