How to Evaluate the Performance of Gradual Type Systems (JFP '19)

Ben Greenman, Asumu Takikawa, Max S. New, Robert Bruce Findler, Jan Vitek, and Matthias Felleisen.
[pdf] [bibtex] [slides] [video abstract] [mp4 source]

Archival version of Is Sound Gradual Typing Dead?. Evaluates the relative performance of different gradual typing systems for the same language, and introduces a method based on simple random sampling to approximate the number of D-deliverable configurations in a program.

The Behavior of Gradual Types: A User Study (DLS '18)

Preston Tunnell Wilson, Ben Greenman, Justin Pombrio and Shriram Krishnamurthi
[pdf] [bibtex] [slides] [data]

Presents the results of surveying professional developers, computer science students, and Mechanical Turk workers on their preferences between three gradual typing semantics.

Collapsible Contracts: Fixing a Pathology of Gradual Typing (OOPSLA '18)

Daniel Feltey, Ben Greenman, Christophe Scholliers, Robert Bruce Findler, and Vincent St-Amour
[pdf] [bibtex]

Design and evaluation of ``space-efficient'' contracts for Racket. Really the contracts are time and space efficient because they are collapsible (i.e. support a merge operation). The implementation is based on Michael Greenberg's model of eidetic contracts.

A Spectrum of Type Soundness and Performance (ICFP '18)

Ben Greenman and Matthias Felleisen
[pdf] [supplement] [bibtex] [slides] [youtube] [src] [redex models] [artifact]

Compares the theory, performance, and implications (for a programmer) of three approaches to adding types to a dynamically-typed language.

On the Cost of Type-Tag Soundness (PEPM '18)

Ben Greenman and Zeina Migeed
[pdf] [bibtex] [slides] [script] [poster] [artifact]

Systematically evaluates the performance of Reticulated. Introduces a method for approximating the number of D-deliverable configurations in a benchmark through simple random sampling. Validates the method with: (1) a tiny bit of statistics, and (2) by comparing some approximations to the ground truth.

Migratory Typing: 10 Years Later (SNAPL '17)

Sam Tobin-Hochstadt, Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Ben Greenman, Andrew M. Kent, Vincent St-Amour, T. Stephen Strickland, Asumu Takikawa
[pdf] [bibtex]

Reflections on Typed Racket.

Type Systems as Macros (POPL '17)

Stephen Chang, Alex Knauth, Ben Greenman.
[pdf] [bibtex] [artifact]

Type systems enforce a syntactic discipline on programmers (language users). Macros systems let programmers (language designers) change the syntax of their language. This paper argues that a macro system is an ideal vehicle for implementing type systems.

Is Sound Gradual Typing Dead? (POPL '16)

Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, Matthias Felleisen.
[pdf] [bibtex] [poster] [artifact]

Proposes a method for evaluating the performance of gradual type systems.

Position Paper: Performance Evaluation for Gradual Type Systems (STOP '15)

Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, Matthias Felleisen.
[pdf] [bibtex] [slides]

Gradual type systems need comprehensive performance evaluation, and this evaluation needs to benchmark all ways of gradually typing example programs. Just checking the fully-untyped and fully-typed versions of a program is not enough!

Getting F-Bounded Polymorphism into Shape (PLDI '14)

Ben Greenman, Fabian Muehlboeck, Ross Tate (and wisdom from the Ceylon team).
[pdf] [bibtex] [poster] [teaser] [slides]

We show how to achieve decidable subtyping in object-oriented languages and argue that our approach is backwards compatible with existing Java projects.

Miscellaneous lecture notes here.