ezyang’s blog

the arc of software bends towards understanding

Galois Tech Talk

abcBridge: Functional interfaces for AIGs and SAT solving

Yesterday I gave a Galois Tech Talk about abcBridge, a set of bindings in Haskell for ABC that I built over the summer as part of my internship. There should be a video soon, but until then, you can download my annotated slides. The software’s not public yet, but hopefully it will be soon.

  • August 25, 2010

Tour of a distributed Erlang application

Bonus post today! Last Tuesday, John Erickson gave a Galois tech talk entitled “Industrial Strength Distributed Explicit Model Checking” (video), in which he describe PReach, an open-source model checker based on Murphi that Intel uses to look for bugs in its models. It is intended as a simpler alternative to Murphi’s built-in distributed capabilities, leveraging […]

  • August 5, 2010

Maximum matching deadlock solution

Last Monday, I presented a parallel algorithm for computing maximum weighted matching, and noted that on real hardware, a naive implementation would deadlock. Several readers correctly identified that sorting the nodes on their most weighted vertex only once was insufficient: when a node becomes paired as is removed from the pool of unpaired nodes, it […]

  • July 16, 2010

Graphs not grids: How caches are corrupting young algorithms designers and how to fix it

Subtitle: Massively multithreaded processors make your undergraduate CS education relevant again. Quicksort. Divide and conquer. Search trees. These and other algorithms form the basis for a classic undergraduate algorithms class, where the big ideas of algorithm design are laid bare for all to see, and the performance model is one instruction, one time unit. “One […]

  • July 12, 2010

Well-founded recursion in Agda

Last Tuesday, Eric Mertens gave the Galois tech talk Introducing Well-Founded Recursion. I have to admit, most of this went over my head the first time I heard it. Here are some notes that I ended up writing for myself as I stepped through the code again. I suggest reading the slides first to get […]

  • June 16, 2010

Static Analysis for everyday (not-PhD) man

Bjarne Stroustrup once boasted, "C++ is a multi-paradigm programming language that supports Object-Oriented and other useful styles of programming. If what you are looking for is something that forces you to do things in exactly one way, C++ isn't it." But as Taras Glek wryly notes, most of the static analysis and coding standards for […]

  • June 9, 2010

Databases are categories

Update. The video of the talk can be found here: Galois Tech Talks on Vimeo: Categories are Databases. On Thursday Dr. David Spivak presented Categories are Databases as a Galois tech talk. His slides are here, and are dramatically more accessible than the paper Simplicial databases. Here is a short attempt to introduce this idea […]

  • June 4, 2010