jrw12@cs.washington.edu
Office: CSE 352
I am a fifth year PhD student interested in programming languages and applications of PL techniques to systems. I'm also a sucker for math, music, and puzzles.
I'm advised by Zach Tatlock in the PLSE group. I am grateful to be supported by a National Science Foundation Graduate Research Fellowship.
I am always looking for undergraduates interested in doing research! Email me!
April 16, 2018.
I have created a list of books I keep in my office. Let me know if you'd like to borrow any!
April 16, 2018.
Our PLDI '18 paper on using modularity to bring decidable reasoning to distributed systems implementations is now available as a pre-print. Check it out!
February 20, 2018.
Next week, I'll be in Vienna presenting our paper
VerifiedFT: A Verified, High-Performance Dynamic Race Detector at PPoPP.
January 1, 2018.
Next week, I will be at CPP, POPL, and CoqPL. At POPL, I will be presenting our paper
Programming and Proving with Distributed Protocols.
At CPP, Eric will present Œuf: Minimizing the Coq Extraction TCB.
Hope to see you there!
December 6, 2017.
Our
paper "VerifiedFT: A Verified, High-Performance Dynamic Race Detector" has
been accepted to PPoPP 2018!
September 26, 2017.
Our
paper "Programming and Proving with Distributed Protocols" has
been accepted to POPL 2018! Check out the preprint!
May 11, 2017.
I just got back from a good time at SNAPL. Check out the slides!
April 21, 2017.
In a few weeks, I will be
at SNAPL to talk
about modular verification of distributed systems.
Hope to see you there!
March 27, 2017.
This coming summer, I will be interning at Microsoft
Research with Jay Lorch and Rustan Leino!
December 30, 2016.
This winter I am teaching CSE 341 (Programming Languages). Check out the
course webpage!
I graduated from Williams College in 2013, where I worked with with Steve Freund. I am now a PhD student at the University of Washington, advised by Zach Tatlock. My work applies programming languages techniques to distributed and multithreaded systems. I especially enjoy proving programs correct.
Outside CS, I enjoy coffee, music, bicycling, and reading. My favorite Seattle coffee shops these days are Vivace in Capitol Hill and Allegro in the U district. The PLSE lab comes in a close third.
For several years, I sang in the UW Chamber Singers. I continue to sing in the St. Marks Cathedral Choir, Evensong Choir, and the Compline Choir. The Cathedral Choir performs each Sunday at 11am at St. Marks. The Evensong Choir performs evensong on the first Sunday of the month, October through May. Both choirs live stream their services here.
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 always thinking about my next tour.
February 21, 2017.
Exercises on Generalizing the Induction Hypothesis.
This post collects several Coq exercises on generalizing the
induction hypothesis.
January 9, 2017.
A Port of the Proof of Peterson's Algorithm to Dafny.
This code-only post is a port of the proof of Peterson's Algorithm to Dafny.
It also serves as a good example of how to reason about concurrent systems
in Dafny, essentially by writing a thread scheduler.
April 24, 2016.
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.
May 8, 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.
April 16, 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.
October 20, 2014
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.
September 14, 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 4, 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.
June 12, 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.
April 10, 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.
March 3, 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.
December 31, 2013
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.
I've had the pleasure of working with the following undergraduates at UW:
In winter 2017, I taught CSE 341 (Programming Languages). Check out the course webpage!
In fall 2013, I TAed CSE 505: Programming Languages with Zach Tatlock.
I have helped run the following reading groups at UW:
I like books. I am guilty of being somewhat more of a collector than a reader, but I don't let that get me down.
I currently have around 120 technical books in my office (listed behind that link). I have another 150 or so technical books at home that are not-so-related to my research, and another 50 or so non-technical books as well. Someday, I'll list them all here.
I am happy to lend books to anyone interested. Just let me know!
I am also very happy to receive recommendations of good books that I'm missing!