James R. Wilcox
he/him or they/them

Assistant Teaching Professor
University of Washington
Office: CSE1 (Allen Center) 440

[email protected]

I am an assistant teaching professor at the University of Washington, where I teach computer science. I specialize in the areas of programming languages and systems.

Before starting on the teaching faculty, I got my PhD at UW and worked in the tech industry for a few years. My research interests are in programming languages and applications of PL techniques to systems. I'm also a sucker for math, music, and puzzles.


News

April 10, 2024.
Our paper "mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic" has been conditionally accepted to the CAV 2024 tools track.

March 18, 2022.
Starting next fall I will continue teaching at UW under the new title of Assistant Teaching Professor!

November 15, 2021.
I am on the academic job market for teaching-track positions this year. I am especially interested in positions at large public universities with a commitment to serving a diverse student population. If you are hiring this year, please feel free to reach out to me.

You can also look at my generic cover letter, CV, teaching statement, and diversity statement. All my materials are also available as a single PDF.


About Me

I am assistant teaching professor of computer science at the University of Washington.

This is my academic homepage. I got my PhD at the University of Washington, where I was advised by Zach Tatlock in the PLSE group. My research interests are in programming languages, systems, and formal methods. My thesis work was on compositional techniques for verifying distributed systems implementations. I generally enjoy working with proof assistants and SMT solvers on applications to all kinds of concurrent programming. I also dabble in floating point, compilers, 3D printing, and database.

Before grad school, I did my undergraduate at Williams College, graduating in 2013, where I worked with Steve Freund on dynamic race detection. Since then Steve and I have continued to collaborate, including on an "our powers combined" paper on verified dynamic race detection with Cormac Flanagan.

Outside computer science, I enjoy good coffee, choral music, distance running, and small planes. I do not enjoy cars of any size.

I sing baritone in the St. Mark's Cathedral Choir, Evensong Choir, and Compline Choir. The Compline Choir performs each Sunday night at 9:30pm at St. Mark's. 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 bike (a Trek 520): in 2009 I biked the TransAm (east to west). I'm always thinking about my next tour.


Publications DBLP Google Scholar


Blog

Subscribe [Valid RSS]

April 29, 2022. (Last updated: October 2024)
Teaching Principles
This living document collects James's Teaching Principles™.

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.



Teaching

At UW:

Service

© James R. Wilcox. Last updated: October 2024