More on GitHub and GitLab.

LTL Instruments

LTL test instruments for three question types: trace-matching, LTL to English, and English to LTL. Read more about them in our Programming 7.2 paper. Used at least once at Brown University and the University of Oxford.

Redex Model of Static Python

Redex model of the Static Python programming language. Helped discover 20+ issues; see our Programming 7.1 paper for more.

Shallow and Optional Typed Racket

racket/typed-racket/pull/948

Two backends for the Typed Racket compiler that change the semantics of types. Instead of the default strong/guarded/deep types, shallow and optional offer weaker guarantees and better performance at boundaries to untyped code. Shallow is inspired by Reticulated Python's Transient semantics. Optional is inspired by TypeScript's static-only types.

Froglet, Forge BSL

tnelson/Forge/tree/dev/froglet tnelson/Forge/pull/120

A small language for software modeling that builds on object-oriented intuitions. Qianfan Chen is the lead author of forge/bsl. Froglet has a type system that enforces OO-idioms (example: . is field access, not relational join) and detects inconsistent bounds.

Collapsible Contracts

racket/racket/pull/2367

An advanced implementation of higher-order contracts (-> and vectorof) that supports a merge operation to save space and checking time without losing blame info. Dan Feltey is the primary author.

Reticulated Performance

Benchmarks, data-collection scripts, data, and a short paper about the overhead of gradual typing in Reticulated.

Gradual Typing Performance

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

Update (2018-04-30): the gradual-typing-performance repo is now split across a few smaller repositories:

There is also a gtp-checkup repo to spot-test new versions of Racket against the benchmarks.

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

docs.racket-lang.org/ipoe

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 compile.sh 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.