My general area of work is in computer science. I currently work at Google, focusing mainly on infrastructure (networking, scheduling, compilers, etc.). I’ve worked academically as an assistant professor of computer science, at Caltech, focusing on methods for high confidence, fault tolerant software, logic, etc. My first job was working at Bellcore (now part of Ericsson) on telecom-related topics.
Programming languages matter. They affect the reliability, security, and efficiency of the code you write, as well as how easy it is to read, refactor, and extend. The languages you know can also change how you think, influencing the way you design software even when you’re not using them.
What makes OCaml special is that it occupies a sweet spot in the space of programming language designs. It provides a combination of efficiency, expressiveness and practicality that is matched by no other language. That is in large part because OCaml is an elegant combination of a few key language features that have been developed over the last 40 years.
Thesis My thesis is about reliable software development, or really about logical frameworks for defining and using new languages and logics. I obtained my Ph.D. from Cornell University in 2000, my advisor is Robert Constable.
Courses I’ve taught courses in operating systems, compilers, theory of computing, computer architecture, etc.
Software that I have written. The following projects have their own sites.
- MetaPRL the logical framework. I originally developed this in grad school as a generic logical framework/theorem prover; It was subsequently developed by many people, especially Aleksey Nogin.
- OMake is a build system designed for scalability and portability. It uses a syntax similar to make utilities you may have used.