David Darais

Principal Scientist - Galois About GaloisGalois tackles the hardest problems in computer science. Our mission is to assure trust in critical systems that protect the privacy and integrity of information in the real world. Core to...

Want to work on programs like VOXLET? Good news: Galois is hiring Principal Scientists!

apply.workable.com/galois/j/4A9...

💡 Academic Tip: always get a haircut the first week of classes.

That way, (1) the students won't think your head is a bird's nest forgotten in the lecture hall, and (2) you can track what's left of the semester by how much you look like a Beatle.

My email got hacked. The damage is limited to the intruder accepting an excessive amount of reviewing obligations on my behalf. Regrettably I will not be able to complete these.

2025 Call for nominations for the Haskell Foundation Hello! everyone The Haskell Foundation’s directors are pleased to announce the nomination process for seats on the Foundation’s board of directors. The board is the ultimate decision-making body of ...

Please consider nominating yourself to be a member of the Board of the #Haskell Foundation: discourse.haskell.org/t/2025-call-...

Making Logical Relations More Relatable (Proof Pearl) Mechanical proofs by logical relations often involve tedious reasoning about substitution. In this paper, we show that this is not necessarily the case, by developing, in Agda, a proof that all simply...

An excellent first introduction to logical relations:

arxiv.org/abs/2309.15724

Very proud to announce that the first Iris paper received the 2025 Most Influential POPL Paper Award this week. This is a testament to the amazing contributions of a wonderful international network of collaborators.

www.youtube.com/live/ZKwpY0g...

I am very happy for @herrdreyer.bsky.social and @natefoster.bsky.social who have become ACM Fellows! Well deserved!

Happy and honored to receive the 2025 ACM SIGSOFT Influential Educator Award! The citation refers to my work on interactive textbooks such as fuzzingbook.org and debuggingbook.org. Thanks to all who helped making this possible!

On my way to POPL! Excited to meet many people I haven’t seen in some time and to hear Noam Zilberstein giving a talk on Demonic Outcome logic, joint work with me, Dexter Kozen, and Joe Tassarotti! Noam will be on the academic market next year, come listen to some of the cool stuff he’s been doing!!

Hot take for POPL: the PL community is still mostly in denial about AI. This is bad because PL+AI go great together

- PL can solve the hardest problem with AI - trusting the output it produces

- AI can solve the hardest problem with PL - finding enough engineers who can even use the tools

This is actually a very good feature to have. Lets you do clean capture avoiding substitution without renaming binders or gensyming new unique variable names.

One week today is the deadline for expressing your interest to attend Programming Language Implementation Summer School (PLISS) -- we have a great program, if I do say so myself! pliss.org/2025/

📢 VerifyThis 2025 - Call for Problems

Submit your interesting academic or industry verification problems to the 2025 edition of the VerifyThis competition (co-located with ETAPS’25) by Feb. 7, 2025! For more information about the competition
& submission process:
www.pm.inf.ethz.ch/research/ver...

@andersmoeller.bsky.social and I are co-chairing OOPSLA'26 and soliciting PC nominations. If you'd like to serve on the OOPSLA PC next year or know anyone (e.g., recent graduate) who you think would do a good job, please nominate them here: forms.gle/NVnzjcmbshoL...

I gave a talk recently about proof technologies - what people deploy today, what might be available soon, and what seems far off even with fancy AI. Slides here: mikedodds.github.io/files/talks/...

AAAI 25 paper Abstract: Datalog is a logic programming language widely used in knowledge representation and reasoning (KRR), program analysis, and social media mining due to its expressiveness and high performance. Traditionally, Datalog engines use ei- ther row-oriented or column-oriented storage. Engines like VLog and Nemo favor column-oriented storage for efficiency on limited-resource machines, while row-oriented engines like Souff´e use advanced datastructures with locking to per- form better on multi-core CPUs. The advent of modern dat- acenter GPUs, such as the NVIDIA H100 with its ability to run over 16k threads simultaneously and high memory band- width, has reopened the debate on which storage layout is more effective. This paper presents the first column-oriented Datalog engines tailored to the strengths of modern GPUs. We present FVLOG, a CUDA-based Datalog runtime library with a column-oriented GPU datastructure that supports all necessary relational algebra operations. Our results demon- strate over 200× performance gains over SOTA CPU-based column-oriented Datalog engines and a 2.5× speedup over GPU Datalog engines in various workloads, including KRR.

Congrats to Yihao Sun (@StarGazerMiao on X :-) on his AAAI '25 paper (his fourth paper this term!). We present our latest GPU Datalog engine, which beats a SOTA CPU-based system by up to 250x, and our previously-SOTA GPU Datalog (ASPLOS '25) by 2.5x. Code is here: github.com/harp-lab/fvlog

Verifying Cake-Cutting, Faster Envy-free cake-cutting protocols procedurally divide an infinitely divisible good among a set of agents so that no agent prefers another's allocation to their own. These protocols are highly complex a...

One of my favourite papers recently: “Verified Cake-Cutting, Faster” arxiv.org/abs/2405.14068

Lindsey Kuper's* group has produced this fantastic zine on choreographic programming that folks should definitely check out: decomposition.al/blog/2024/12...

(* can't seem to find Lindsey here but please tag if you know the handle)

The Hoare Cube I wrote earlier this year about my attempt to understand the repercussions of toggling $latex \subseteq$ and $latex \supseteq$ when giving a semantics to Hoare triples. In response to that post, Ya…

Program correctness and incorrectness are not just two sides of the same coin; they're two faces of the same cube! johnwickerson.wordpress.com/2024/12/04/t...

Me in 2021: oh look, PL folks are all arguing about whether or not the word “transpiler” should exist on Twitter. Always good fun!

Me in 2022: ew, Elon bought Twitter, I’m out.

Me in 2024: bluesky looks fun. PL folks must have moved on to arguing about something else… Let’s log on and find out!

What could be simpler? 5 mode axes and 11 distinct modes. Nothing to worry about.

PLDI 2025 Artifact Evaluation Committee Self Nomination This form allows any member of the community to nominate *yourself* to be part of the Artifact Evaluation Committee for PLDI 2025. While we cannot select all qualified candidates, we will do our best ...

Attention🚨 We are looking for motivated students and researchers to be members of the PLDI 2025 Artifact Evaluation Committee. This year, we are accepting self-nominations (the form is here: forms.gle/2TPmixasDmqM...). Deadline: Dec 23rd, 2024.

For more info: pldi25.sigplan.org/track/pldi-2...

this is one of my favorite custom feeds, Quiet Posters

it shows you posts from people you follow who don't post that much! so it surfaces friends' posts that might otherwise get drowned out in the Following feed (which is reverse chronological) 🤗

This talk from Jonathan Ragan Kelley highlights the basic pressure around parallelism and hardware, and the coevolution of hardware (particularly GPUs) and parallel programming paradigms, as well as some directions for us to go next. Great talk.

youtu.be/vU3ryvZYlkk?...

How to Compare Fuzzers SAPLING'24

My talk "How to Compare Fuzzers" at SAPLING'24 yesterday is available on line here: speakerdeck.com/rahulgopinat... #SoftwareEnginnering #MutationTesting #Fuzzing

The preprint of our ASPLOS '25 paper, "Optimizing Datalog for the GPU," is here: arxiv.org/pdf/2311.02206

My postdoc Charlie Murphy is on the academic job market this fall. He's doing really hard technical work on building constraint solvers and synthesis engines. You should interview him
pages.cs.wisc.edu/~tcmurphy4/