Deep and Shallow Types (Ph.D. dissertation, December '20)

Ben Greenman
[pdf] [bibtex] [slides] [youtube] [src]

Presents four contributions: (1) a systematic method to evaluate the performance of a mixed-typed language; (2) formal properties that measure the strength of types; (3) a scaled-up Transient semantics; and (4) the design and implementation of a language that combines Deep types (complete monitoring), Shallow types (type soundness), and untyped code. The combination helps avoid many worst-of-both-worlds situations that arise with Deep types only or Shallow types only.

Complete Monitors for Gradual Types (OOPSLA '19)

Ben Greenman, Matthias Felleisen, and Christos Dimoulas
[pdf] [supplement] [bibtex] [slides] [youtube] [src]

Adapts complete monitoring into a (syntactic, operational) proof technique for migratory typing. A semantics satisfies complete monitoring iff it protects all channels of communication between typed and untyped code. Introduces blame soundness and blame completeness to test whether systems that fail complete monitoring can identify exactly the codes responsible for a run-time type mismatch.

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

Ben Greenman, Asumu Takikawa, Max S. New, Daniel Feltey, 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.

Note: The data for the zordoz benchmark is flawed; in fact, there is little improvement between v6.2 and v6.4 on this benchmark. For details, see the release notes for version 3 of the GTP benchmark suite.

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.

Update 2019-11-13: as it turns out, the paper describes a complete spectrum in ye olde "data processing" sense (Kelly-Bootle, Stan. The Devil's DP Dictionary. McGraw-Hill Inc. 1981).

spectrum n. plural spectrums; mandatory DP usage wide spectrum(s). [Latin spectrum "an apparition."] Any range of one or two items or features.

† A range of from three to seven features (the legal maximum) is known as a complete or total spectrum. Ranges of eight or more are called unfair trading.

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.