Weak but Functional Pigeons

A bird's eye view of [Razborov, Resolution Lower Bounds for the Weak Functional Pigeonhole Principle, 2003].

LYM Inequality

A simple proof.

Cap Sets

Why it's difficult to avoid arithmetic progressions.

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.

Coverability for Vector Addition Systems

Vector addition systems are a model of computation. For this model, coverability is one of the easiest decision problems. This post presents an old (1978) upper bound, with accompanying code.

Beta Function

How to compute $\int_0^1 dp\, p^k(1-p)^{n-k}$ without symbol manipulation.

Watching Horn

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

Coursera Courses

In this post I review some of the Coursera courses that I completed.

At Most R

How to encode a cardinality constraint as boolean constraints.

IMO 2014 problem 1

This is an exercise proposed by Timothy Gowers: Write down all you think of while trying to solve a math problem.

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.

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.

Approximation of Binomial Coefficients

A proof that $\frac{1}{2}\frac{n^k}{k!}\lt{n\choose k}$.

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.