Finite-choice logic programming @ POPL

This week, on stage with Chris and Michael, I presented our work on Finite-Choice Logic Programming, the theory behind our Dusa logic programming language. There were hats involved, as captured in this beautiful image from Katherine Philip.

(Special thanks to Ron who stole the show in his pivotal role as a very convincing heckler, captured on BlueSky here.)

I’ll update this post once the video is cropped out of the livestream and posted on the SIGPLAN YouTube page. However, if you weren’t there, the best presentation is probably this PDF with lightly edited slides and a minimally edited transcript of the talk. The full story, of course, is in the paper.

I hope we communicate why we’re interested in the principles underlying this new programming language. The talk barely mentions the Dusa implementation; instead, it focuses on how we were able to define the meaning of programs as a potentially-infinite set of solutions, all of which disagree with each other. I’ve been describing our central mathematical construction — defining a complete lattice of sets-of-incompatible-sets-of-facts — as “just annoying enough that I understand why nobody else did it before” (at least nobody else, to our knowledge, did it to solve the problem we were solving). But now that we’ve written this out, I hope it’s a chunk of math that others will find useful in other work!