Gradual Typing Performance

Our home for work on improving the performance of gradual type systems. Contains benchmarks, publications, developer tools, and experiments.

trivial: Observably Improved Type Checking

A library of local, composable syntactic analyses. We propagate facts about constant values in the program to standard library functions and generate annotations for the type checker. The library documentation has examples.

Running the Typed Racket type checker on existing Typed Racket code detects more errors and accepts more correct programs when this library is imported. Importing shadows existing function calls, replacing them with type-annotating elaborations.

Interactive Poetry Editor

Implements an extensible family of languages for checking correctness properties of poems. For instance, we have a little checker for haikus and another for sonnets. These are defined through a uniform specification language, which compiles its programs into specific poetry-checking programs.

The "interactive" part is very important. Unless told otherwise, the checker will actively search for new words and keep a dialog with the user. Next up is learning some rules of English based on these interactions.

Java Corpus

A collection of open-source Java projects, gathered while I was working on the shapes paper. Each project is in a separate folder, and each folder contains a small script. These scripts are direct calls to javac, so it's very easy to swap in your own compiler.

Racket Bytecode Explorer

A small REPL interface to Racket bytecode (.zo) files. Has a string-based search features, and can be called from the command-line to give a count of AST nodes' frequency.

OCaml Command Line Interface

Courseware for CS 3110 at Cornell. Streamlines compilation and unit testing for students (no need to call ocamlc!), and helps staff with grading; in particular running and collecting statistics on a test suite and emailing students if their submission failed to compile.