The Nautalis in Vedauwoo, Wyoming
Me, playing around in Rocktown, GA

Clay Thomas

I'm a PhD student in the Computer Science Theory group at Princeton University. I'm broadly interested in problems with computational applications and an algebraic feel. I completed my undergrad in Mathematics and Computer Science at Purdue University, where I was fortunate to be advised by Elena Grigorescu.

My other interests include rock climbing, gymnastics, and teaching.

Here's my CV

Publications

V. Gandikota, E. Grigorescu, C. Thomas, and M. Zhu. Maximally recoverable codes: The bounded case. In Allerton Conference on Communication, Control, and Computing, 2017. [paper] [slides]

Modern distributed storage systems employ Maximally Recoverable codes that aim to balance failure recovery capabilities with encoding/decoding efficiency tradeoffs. Recent works of Gopalan et al (SODA 2017) and Kane et al (FOCS 2017) show that the alphabet size of grid-like topologies of practical interest must be large, a feature that hampers decoding efficiency.

To bypass such shortcomings, in this work we initiate the study of a weaker version of recoverability, where instead of being able to correct all correctable erasure patterns (as is the case for maximal recoverability), we only require to correct all erasure patterns of bounded size. The study of this notion reduces to a variant of a combinatorial problem studied in the literature, which is interesting in its own right.

We study the alphabet size of codes withstanding all erasure patterns of small (constant) size. We believe the questions we propose are relevant to both real storage systems and combinatorial analysis, and merit further study.

Projects

Verifying Structural Invariants of Programs

[report] [slides]

For my Reasoning About Programs course, I've been working on the problem of verifying structural invariants of programs. Our two key examples, and those we've had the most success with, are invariance under the ordering of a list and invariance under equivalent binary search trees. For both of these data types, we've found simple permutations that "generate" all equivalent data types, in the sense that applying those permutations in some order to any data structure can result in all structures equivalent to the input. We also have a more general, sound procedure that can verify the invariance of an arbitrary data type under some underlying representation (for example, a function on binary search trees should be invariant under the function "list" that returns the ordered list corresponding to the tree). However, our procedure includes an inductive synthesizer and an equivalence-of-programs verifier in its inner loop, so it may not be very practical.

Teaching

I enjoy lecturing and explaining foundational concepts. Furthermore, I like writing challenging and interesting practice questions for students (including thinking of exercises for myself!).

When I TAed for Purdue's "Foundations of computer science" course, I wrote some lecture notes for a few of my "practice, study, observation" sessions and I wrote review materials for the midterm and final. You can find those materials here.

Haskell

My manager at Facebook told me that there's an old saying among Haskellers: "The best way to learn monads is to write a monad tutorial, then throw it away" because nobody else will ever find it useful. Personally, I think monad tutorials are a myth. Writing a monad tutorial is like writing a "data structures" tutorial or a "programming patterns" tutorial: way too broad. Anyway, here's my monad tutorial.

I want make some simplified versions of Haskell libraries that are easier to understand so people can learn the concepts of the libraries. Here's the start of that project for the Lens library.

Here's the "free decision trees" blog post (see project section below).

Smaller Independent Projects

These are all smaller, simpler, code-based projects which I wrote independently.

Ramsey Languages

January 2017. Haskell implementations of a simple imperative programming language and a simple Lisp. Based on operational semantics from Norman Ramsey's book Programming Languages: Build, Prove, Compare.

Fair Read-Write Locks

March 2016. A kernel-level read-write lock implementation in the Xinu operating system, giving readers and writers access in exactly the order they request it.

This small project inspired a question I really want to come back to one day: Are all synchronization protocols implementable with common sets of synchronization primitives? For example, is it possible to implement fair read-write locks using only semaphores? No implementation I have seen is actually fair in the sense discussed above. See the repo for more information.

Free Decision Trees — Library and Blog Post

January 2016. A rudimentary library to train and apply decision trees represented in an elegant way. This project was inspired by the observation that the Haskell data type Free ((->) r) Bool could be used to represent decision trees. The result is a blog-post style explanation of the concept and implementation, which I think is a good way to understand free monads. You can find the reddit discussion here.

Joy Interpreter

August 2015. A small, toy interpreter for the stack based functional language Joy. Written in Haskell.

Haskell algorithms

April 2015. Implementations of a heap based priority queue, red-black trees, prefix trie, suffix trie, find-union of sets, and finding minimal spanning trees.

ForceBoard

2013. A Java application for simulating the motion of objects influenced by gravity, springs, drag, etc.

Simple Deriver

2012. A Java application that parses equations, symbolically derives them, and plots the result.

Other Things

Here's a hackathon project I worked on to help you meet your friends at different Purdue dining courts.

Here's a Purdue problem of the week from back in the day. Here is a partial graph of the function constructed, where I enumerated rationals in some simple order and plotted the value of the function there. Seems like the graph is dense in the plane, but I don't think I even knew what "dense" meant at the time.

Here's an image I made to explain how to derive an equation of the form z = f(x,y) for the graph of a Torus.

Here's a little writeup of a counting problem that I found tough and interesting at the time.

Here's a writeup I did when I took physics about the fact that objects always roll down slopes with less acceleration than if they were slipping down the slope without rolling. I also construct shapes with acceleration arbitrarily close to the "slipping acceleration".