More on GitHub and GitLab.
Visual Studio Code plugin to ask GPT a question from your editor.
UI example here: [pdf].
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 the Static Python programming language.
Helped discover 20+ issues; see our Programming 7.1 paper for more.
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.
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.
Benchmarks, data-collection scripts, data, and a short paper about the overhead of
gradual typing in Reticulated.
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.
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.
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.
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.
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.
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.
Gradual Typing Performance