An Introduction to Formal Methods
This is a somewhat narrow introduction to formal methods I presented at UCLA in March of 2022 with the goal of describing some of my research at Sandia.
Assistant to the Proof Assistant
Writings on computer stuff.
Latest posts
Compiling Volatile Correctly in Java
The compilation scheme for Volatile accesses in the OpenJDK 9 HotSpot Java Virtual Machine has a major problem that persists despite a recent bug report and a long discussion. One of the suggested fixes is to let Java compile Volatile accesses in the same way as C/C++11. However, we show that this approach is invalid for Java. Indeed, we show a set of optimizations that is valid for C/C++11 but…
Formalizing Java's Access Modes
This is my presentation from OOPSLA 2019 on our formal model for the Varhandle API in JDK 9. More information on the paper can be found here . The Coq source and our Herd model/tests have been made available as well.
NP-complete: how hard is that climb?
The purpose of this post is to clarify the difference between NP -hard and NP -complete problems for developers who, like me, have found that the abstract nature of the definitions make developing an intuition for it difficult. Climbing a Mountain # Imagine that a friend came to you and said that she would like you plan a trip up an obscure mountain, X . Obviously you need to know how difficult…
Differential Semantics
A quick presentation I gave to my CS 239, Spring 2014 on my early thinking around deriving programmer intent from source control and program evolution.
A Better SQL
The relational model for data is ubiquitous. That's in part due to SQL's declarative approach to manipulating and exploring data stored as relations. Unfortunately SQL has its warts. In particular schema changes made in the data definition subset of the language (DDL) [1] can be awkward for creating idempotent migrations. Enough so, that the responsibility is frequently delegated to the…
Why I'm Getting a PhD
The 26th is the first day of instruction in the first academic year of my PhD in Computer Science at UCLA. I have a two year old daughter, an incredibly supportive wife, and I just turned 30. Unsurprisingly, I've been asked many times why I want to get a PhD and I rarely get a chance to explain my thinking fully. This post is both a detailed account of my reasons and a counterpoint to the popular…
Faster JavaScript through Category Theory
Update My final presentation of the material from JQuery UK has been posted. On a personal note the venue and speakers made for an awesome setting to retire this talk. View video on Vimeo Update My presentation of the revised material from JSCONFEU 2012 has been posted. Thanks again the @jsconfeu crew for puting on one of the best conferences I've yet been to. View video on Youtube My presentation…
Splitting jQuery in Two, A Proposal
Previously I've described applications of Category Theory in JavaScript and with jQuery. An earlier post, Faster JavaScript with Category Theory , identified a possible performance benefit where composition could be shown to hold for a Functor from Html to Jqry . This post follows up with a more concrete look at that optimization and suggests an additional, farther reaching, implication for the…
A Natural Transformation in JavaScript
Natural transformations are a foundational construct in category theory, so it seems fitting to follow up my last post by describing one using the categories Html and Jqry . As a result this post assumes the reader has covered the material from the last post. Also, as much as I wish that I could claim a similarly exciting result this will remain mostly an exercise in clarifying what natural…
Faster Javascript Through Category Theory
This post started out as a gist that I was using to work through what I've learned about category theory by applying it to something I already know: JavaScript. The surprising result was a clearly defined set of JavaScript functions and jQuery helpers that could be optimized to reduce execution time. In the course of this post we'll define two categories: one for HTMLElements and the other for…