Silence, and adding things up

Well, so much for new year resolutions . I’d like to claim I haven’t posted anything for a while because I’ve been being super-productive, but I think it’s more due to teaching and not paying much attention to blogland. Perhaps there will be more brain dumps when the students have gone…

Anyway. We’ve just submitted a paper on the carry ripple adder for binary numbers, using dependent types, to TFP 2007.

The brief summary is this: instead of writing the binary adder directly, and proving important properties such as commutativity, associativity etc directly, we write an addition function inductively over natural numbers, then the properties we care about are easy to show by induction. To write the binary adder, we construct a representation of binary numbers indexed over the natural numbers, so each binary number has an explicit decoding as a natural number visible in its type, and declare that the decoding of the addition of two binary numbers is the sum of the two decodings. If we can write such a function, we have a binary adder with all the properties of the natural number addition for free.

We’re using dependent types to give an explicit and machine checkable link between a high level implementation where correctness properties are easy to show, and a low level implementation which is something we’re more likely to want to implement in real hardware but is hard to reason about. I’m always on the lookout for more concrete problems along these lines, please let me know if you can think of others!