James R. Wilcox

PhD Student
Computer Science and Engineering
University of Washington
Office: CSE 352

My Calendar

I am currently (always?) looking for motivated undergraduates who are interested in doing research! Contact me to learn more!


We have a new paper on our verified implementation of Raft! I'll be presenting it at CPP in January. Hope to see you there! —December 8, 2015

This week I'm in Lincoln, Nebraska, (commonly referred to as the "Silicon Prairie") to attend ASE. I'll be talking about SlimState, which is a technique for handling array shadow state efficiently in dynamic analyses. —November 10, 2015

I'll be attending PLDI in Portland this week. Check out our projects Verdi and Herbie! Come to the talks and chat with us afterwards! —June 13, 2015

Verdi has a website! Also check us out on github! —April 16, 2015

Verdi, our project on verified distributed systems, is open source! There will be more documentation and web presence soon, but in the meantime, comments and pull requests are welcome! —February 10, 2015

We had two papers conditionally accepted to PLDI 2015! See the publications section for details. —February 4, 2015

The PLDI deadline has passed, and I've fully recovered. Text was written. Papers were submitted. We'll see what happens! —November 20, 2014

Summer is over. Fall quarter is almost here! I'm a second year. (!!) This fall I'll be taking grad Systems with Arvind, plus every grad level class offered by Xi or Emina (whenever those get settled). Pavel and I are thinking about reading parametricity papers; let us know if you're interested. —September 4, 2014

I am attending OPLSS in Eugene, OR, June 15-29. Hope to see you there! —June 12, 2014

Spring Quarter is here! I'm very happy to not be taking any courses. I'm also excited to be organizing a reading group in categorical models for typed lambda calculi. There's a webpage. —April 10, 2014

I'm organizing the HoTT reading group. There's a webpage. —February 3, 2014

Winter (quarter) is coming! I'm excited to have a PL-filled course load coming up. This is me rebelling against my well-rounded liberal arts education, or something... To top it all off, I'm thinking of organizing a "classic PL" reading group. Let me know if you're interested! —December 31, 2013

I am singing with whateverandeveramen, a project-based choral group. On February 7, 2014, at 7:30pm, in University Presbyterian Church, we're singing the world premiere of "Songs of Fatherhood" by David Montoya with poetry by William Wallis. You should come! —December 20, 2013

I am attending PLMW/POPL, January 20-25, 2014. Hope to see you there! —December 20, 2013

About Me

I am a third year PhD student in the Computer Science and Engineering department at the University of Washington. My interests are in programming languages and applications of PL techniques to systems. I'm also a sucker for math and puzzles.

I'm advised by Zach Tatlock in the Programming Languages and Software Engineering (PLSE, pronounced "pulse") group. I am grateful to be supported by a National Science Foundation Graduate Research Fellowship.

I graduated from Williams College in 2013 with a lot of great friends as well as a B.A. in Computer Science and Mathematics. I did research with Steve Freund (Summer 2012, Fall 2012, and Spring 2013) and Duane Bailey (Winter 2011). In summer 2013, I worked for NVIDIA as an intern in the research division under David Luebke and Morgan McGuire.

Outside CS, I enjoy coffee, music, bicycling, and reading. My favorite Seattle coffee shops these days are Roy Street in Capitol Hill and Allegro in the U district. The PLSE lab comes in a close third.

I sing in the UW Chamber Singers, the St. Marks Cathedral Choir, and the Compline Choir.

The Chamber Singers were excited to perform at the ACDA Northwest conference in March, 2014. You can see videos of our performance here, here, here, and here. We are also working on a CD with repertoire from the 2013-2014 and 2014-2015 seasons. The Cathedral Choir performs each Sunday at 11am at St. Marks.

The Compline Choir performs each Sunday night at 9:30pm at St. Marks. The compline service a 30 minute chanted/sung service that tends to draw hundreds of people every week and thousands via a live radio broadcast and the podcast. It's a classic Seattle experience. You should check it out! You can listen live on King FM or get the podcast.

I occasionally play handbells.

Finally, I like to ride my 2009 Trek 520 bicycle: in 2009 I biked the TransAm. I bike from Ballard to CSE most days on the Burke-Gillman. I'm thinking about buying a mountain bike and biking along the Adventure Cycling Great Divide Trail in August 2015.

In non-fiction, I enjoy philosophy and popular science books. I recently read and enjoyed Jonathan Haidt's The Righteous Mind. In fiction, I like short stories and (not exactly fiction) essays by people who write good short stories. Recent favorites include George Saunders' The Braindead Megaphone.



How to build a simple system in Verdi. In this long-awaited post, we'll show how to implement and verify a simple distributed system using network semantics. —April 24, 2015

A Proof of Peterson's Algorithm. In this post, we take a break from distributed systems to look at shared memory systems. As a case study, we give a proof that Peterson's algorithm provides mutual exclusion. —May 8, 2015

Network Semantics for Verifying Distributed Systems. This is the first post in a series on Verdi. In this post, we'll get our feet wet by defining a formal model of how distributed systems execute on the network. —April 16, 2015

Reasoning about Cardinalities of Sums and Products. In this short, code-heavy post, we extend some of the work from a previous post to reason about the cardinalities of sums and products. —October 20, 2014

Dependent Case Analysis in Coq without Axioms. This post shows how to get around the limitations of the destruct tactic when doing case analysis on dependent types, without resorting to the dependent destruction tactic, which relies on additional axioms. —September 14, 2014

"run" + "time" = ???. This brief post records Mike's description of the three ways of combining the words "run" and "time" in computer science writing. —September 4, 2014

"More Sums than Differences" Sets, Part 2: Counting MSTD Sets. This is the (much delayed) second post in a series on More Sums than Difference Sets. In this post, we'll take a first crack at the question, "How many MSTD sets are there?" To do so, we'll write a straightforward C program that counts MSTD sets. Then we'll run it to count MSTD sets and benchmark its performance. —June 12, 2014

Tail Recursion Modulo cons. Tail recursion has come up in a few conversations this week. This post explores a generalization of tail call optimization that I wasn't aware of until Doug described it to me. —April 10, 2014

"More Sums than Differences" Sets, Part 1: A puzzle. This is the first post in a series on "More Sums than Differences" Sets. In this post, we'll get our terminology straight and ask a lot of questions. —March 3, 2014

Easy access to the off-campus proxy. I use the UW proxy to access the ACM digital library from off campus, but it's annoying to type the proxy URL every time I click a link to a new paper. Here are two ways to make life easier. —December 31, 2013

Publications (DBLP)

In Peer-Reviewed Journals

In Peer-Reviewed Conferences

In Peer-Reviewed Workshops

Theses, Tech Reports, Preprints, and Other Non-Peer-Reviewed Papers

Talks and Poster Sessions


I've had the pleasure of working with the following undergraduates at UW:



In fall '13, I TAed CSE 505: Programming Languages with Zach Tatlock.

I have helped run the following reading groups:

At Williams

I TAed my last 7 out of 8 semesters at Williams. Here's a partial list of courses I TAed for:



At Williams

I took a lot of CS and math, a smattering of music and philosophy, as well as a few other things. Some highlights include:
Website template/design shamelessly stolen from Zach Tatlock.
(c) James Wilcox. Last updated: April 25, 2016.