The Standard Stuff

• My publications
• As BibTeX
• At Google Scholar
• At DBLP
• ACM author profile
• My CV
• In PostScript
• In PDF
• Coauthors index
• LinkedIn profile

Draft Papers

• Syntactic Proofs of Compositional Compiler Correctness

Software

• Cooperative Internet hosting tools, including DomTool, a domain-specific language in support of shared UNIX system configuration by mutually-untrusting users
• Dynamic web site tools for Standard ML, including separately usable libraries for accessing SQL databases
• Links to sundry other projects can be found from my SourceForge profile.
• Most of this web site is built from an XML database using XSLT. I've published my code for doing this.

Photos

• SPLASH 2016
• APLAS 2016
• NDIST 2016
• POPL 2017

...and All the Rest

• Coq class at Harvard, from Fall 2008
• Course on Interactive Computer Theorem Proving (focusing on Coq) that I taught in Fall 2006
• A point-by-point comparison of the Objective Caml and Standard ML programming languages
• Challenge problems and solutions that I've posted on the POPLmark mailing list
• Looking for Internet hosting where you can go wild developing Internet services with your favorite non-mainstream programming language? Join HCoop, the Internet Hosting Cooperative!
• My personal web site
• Archival version of my last web site at Berkeley
• Academic genealogy
• Best upper bound on my Erdös Number that I know of: 3