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

Ben Greenman and Matthias Felleisen
[pdf] [supplement] [bibtex] [src]

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.