Typed unit calculi prove that well-typed programs are invariant under rescaling: no program can depend on how big a meter is. They obtain this by admitting no operation that can observe a unit, and so no conversion. Practical languages provide conversion but no invariance theorem. Λs has both. It is a typed lambda calculus in which conversion between units of the same dimension is a primitive, and it determines exactly how much invariance survives.
The repository is the artifact of the paper A Calculus for Units of Measure with Conversion: the full Lean 4 mechanization of the statics, dynamics, and denotational semantics, two abstraction theorems, a decidable diagnostic for conversion drift, a verified checker for unit declarations, adequacy, erasure, and the Pi theorem of dimensional analysis. The evaluator compiles to a native binary.
Towel previewing a refactoring of a 16-line file. Half a minute, silent. The output and the wait are those of a real run; the highlights and captions are added. Transcript.
Towel finds repeated Python code and extracts it into shared helper functions. It checks each extraction, preserves the parts that differ as parameters, and leaves meaningful names for you to choose.
The method is anti-unification. Given two fragments of code, Towel computes their least general generalization: the most specific template of which both are instances. The template becomes the helper, and the places where the fragments differ become its parameters.
Project Fortress
A programming language for high-performance computing · Sun Labs, 2003–2011
Many, but unfortunately not all, of the key contributors to Fortress, including several summer interns who have since gone on to do great research.
Project Fortress was an initiative at Sun Labs, sponsored by DARPA HPCS, to develop a next-generation high-performance programming language. Fortress was designed to enable programming at the peta-scale: petaflops of compute and petabytes of memory, orders of magnitude beyond the fastest computer in the world at the start of the project. I joined the team at the start and had the honor of working with many outstanding researchers, including Guy L. Steele Jr., a longtime hero of mine, and Steve Heller, with whom I worked for almost two decades at Sun Labs and Two Sigma.
Originally we referred to the language as “secure Fortran,” even though, semantically and syntactically, it was nothing like Fortran. The name Fortress came to me in the middle of the night as a pun on that phrase; I was so amused with myself that I had to get up and write it down. I suggested it to the team as an internal codename, and the name stuck.
Fortress was an open source project, and a significant amount of technology was released over its lifetime. I keep a repository of the published material: source code, supporting documents, and tools.
DrJava
A lightweight pedagogic environment for Java · Rice University
DrJava is a lightweight development environment for Java, built for teaching. My PhD advisor, Robert Cartwright, Brian Stoler, and I designed it at Rice, taking its pedagogic approach from Racket. Its interactions pane is a metacircular interpreter that calls out to JVM primitives, so Java code can be evaluated as it is written, with every Java library at hand. We released it as open source and, with Charlie Reis, continued its development through a Rice course in production programming.
