Picture of Chris Stone


Christopher A. Stone

Email: stone@cs.hmc.edu
Phone: (909) 607-8975
Admin:   (909) 621-8225
Fax: (909) 621-8465
Office: Olin B157


What are you doing this semester?

During Spring 2018, I am teaching CS 132: Compiler Design and co-teaching CS 131: Programming Languages with Prof. Melissa O'Neill. I'm also as advising a Clinic team of four students who are working on a project for Lawrence Livermore National Laboratory.

My official office hours are Tuesday 1-2pm, Thursday 3-4pm, and Friday 10-11am. You can also drop by my office at other times (since my door is often open in the afternoon) or email me to make an appointment. My weekly schedule suggests when I'm most likely to be available.


Is decidability overrated? (Or:Is there a difference between “equal by definition“ and “provably equal”?

While finding a proof of a theorem may be hard, checking that a well-written proof is free of errors if the proof is well-written then checking that it's free of errors (that Type Theory blurs the lines between mathematical proofs and executable programs, and is the basis of most systems for creating computer-checked proofs. Such systems distinguish between definitional/judgmental equality—two ways of writing the obviously the same thing, like 3+1 and 4— and provable/propositional equality—equalities that must be justified by a proof.

The dividing line is not always clear. For example, if rev is a function for reversing lists, then obviously rev(rev(l)) == l; are these just two ways of describing the same list, or is simplifying rev(rev(l)) to l a step worth noting?

Most computer-assisted proof systems have some fixed definition of definitional equality built in; everything else requires proof. Prof. Andrej Bauer and I are looking at more flexible systems where the definition of definitional equality can change as needed, in the context of a particular system called Homotopy Type Theory (HoTT).

More information on HoTT »

Why can't humans and computer read the same proofs?

Errors in software become more expensive and dangerous each year. Testing is helpful, but proofs are the only way to truly guarantee that an algorithm is correct, or that a cryptographic protocol is secure, or that a programming language is safe.

Unfortunately, it’s hard to get all the details of a big proof right; even careful reasoners make mistakes, and even careful readers miss them. Automation seems a natural solution, and there exist “proof assistant” systems to help people construct and verify proofs, using special-purpose computer languages. In the end, though, we have a proof that we are sure is correct but that is almost unreadable if you’re not a computer!

I want a system that can verify proofs that were written for humans to read and understand, the kind of proofs you see in textbooks and research papers. Essentially, I want to go beyond spell-checking and grammar-checking to logic-checking.

Matt Valentine and I started looking into this during Summer 2014, and I hope to continue this line of work.

Summer Plans in More Detail »

Does programming multicore CPUs have to be so difficult?

Multicore processors are ubiquitous in desktops, laptops, and even cell phones have multicore processors, yet they are still too hard to program. The most common approach involves “locks,” which are tricky and error-prone (not enough locks → race conditions; too many or out of order → deadlock). Newer techniques like Transactional Memory can be awkward to use.

Observationally Cooperative Multithreading (OCM) is an approach to parallel programming that I have been investigating with Professor Melissa O'Neill and an impressive series of 33 undergraduates over the past seven years.

We start with classical Cooperative Multithreading (CM), where only one thread runs at a time, and each thread gets the whole machine to itself until it explicitly yields control to the next. CM is a very convenient programming model; if threads are only interrupted when they choose to be, then locks and the problems that go with them can largely be avoided.

OCM lets us write programmer-friendly CM code, yet still advantage of multiple processors. Code runs “as if” one thread were running at a time. But when two threads are independent, an OCM system can run them simultaneously to get the same answer, but faster!

To learn more about the OCM model, I recommend starting with this (unpublished) introduction to Observationally Cooperative Multithreading. Our best implementation is described in the TRANSACT 2015 paper Making Impractical Implementations Practical: Observationally Cooperative Multithreading Using HLE.

How could a set be finite without having a size?
Lists are easy; what does it mean to “code up” a smooth manifold, or the mathematical set ℝ?

The RZ system translates specifications for mathematical structures into specifications for code. It answers questions like, "What would a programmer need to implement in order to get a complete and correct implementation of the mathematical (“real”) real numbers [ or of a compact metric space, or a space of smooth functions, ...]?"

From an educational perspective, it also provides explanations (in terms a programmer can understand) of the non-classical distinctions that arise in constructive mathematics. For example, it can be used to explain the difference between a finite set and a set that is not infinite, and why there is a "size" function only for the former.

More information on RZ »

What else have you done?

You can look a list of selected papers and talks or my full CV.

Code and Other Artifacts

Where can I find a C++11 implementation of Bond et al.'s Octet locks?

I'm glad you asked! I put together an implementation as an offshoot of the OCM research project.

Octet locks are interesting for concurrent programming because threads aren't required to unlock when they're done; this can be a big speed advantage for resources that are accessed mostly by a single thread. Further, Octet locks can be acquired in any order without fear of deadlock (though while acquiring one lock you might lose others).

Github repository »

How can I convert a bunch of Microsoft Word files to PDF?
How can I convert a bunch of Omnigraffle diagrams to PDF and PNG?
Can I use short URLs (like www/wiki instead of www.cs.hmc.edu/wiki) in Safari?

Teaching occasionally requires some tedious tasks, so I've thrown together small utility programs (for Mac OS X).

Details and downloads »

Where can I find more examples from your Random Art assignment?

Some of my favorites appear on the official SIGCSE Nifty Assignments web page for Random Art. I've also put together a PDF poster containing nearly all the student-generated pictures that I've collected while teaching CS 131: Programming Languages.

Of course there's also the original Random Art webpage, which inspired the CS 131 assignment.

Some Random Art


My wife Sneža is a private French tutor, who works with students remotely via Skype. I am very proud that she has written a number of successful e-books for learning French, including including Exercise Your French: Grammar & Exercises, a 390-page book of French grammar explanations and 1800 exercises (with full solutions). Her other e-books contain stories in French (with English translations and vocabulary notes, and in several cases, MP3 recordings), including Exercise Your French: Read and Listen and Le nouveau voisin: French for Beginners and Le sac à dos oublié: French for Beginners and Alvin et Mimi: French Short Stories (Beginner Level) and Alvin et Mimi: French Short Stories (Intermediate Level).