Three Approaches to Gradual Typing (November 2018)

Presented at GRACE 2018

High-level summary of our recent work. Describes three strategies for migratory typing (i.e., adding types to a dynamically-typed language) and their implications for soundness, performance, and developer preference.

A Spectrum of Type Soundness and Performance (August 2018)

Presented at NEPLS 32

Shows (1) a way to group ``gradually typed'' languages by their semantics --- in particular how they enforce types at the boundary between typed and untyped code --- and (2) results from an evaluation comparing the three semantics as three ways of running a set of Typed Racket programs.

A Spectrum of Soundness and Performance (April 2018)

Presented at a PI meeting for the NSF grant Gradual Typing Across the Spectrum.

Three ways of looking at type soundess for a pair of languages.

Transient Racket (August 2017)

Presented at a PI meeting for the NSF grant Gradual Typing Across the Spectrum.

Answering the question: "why implement tag-level type soundness for Typed Racket?"

Measuring Reticulated Python (June 2017)

Presented at NEPLS 31

Reticulated is an implementation of sound gradual typing for Python. This talk explains two points: (1) the soundness guarantee is very weak compared to standard, strong type soundness; and (2) the run-time cost of enforcing soundness is low.

On Gradual Typing Performance (May 2016)

Presented at a PI meeting for the NSF grant Gradual Typing Across the Spectrum.

Our 2016 paper Is Sound Gradual Typing Dead? introduced a graphical shorthand for describing the performance of a gradual type system. These slides explain the practical experience that led us to the shorthand.

A Case for Sound Gradual Typing (February 2016)

Presented at a little ECOOP'16 PC weekend of talks.

Sound gradual typing is not about catching more run-time errors at compile-time. Rather, the goal is to provide the minumum safety guarantees for a trustworthy type system in the presence of unchecked code. If the types are not protected at runtime, there is a risk for silent errors.

A #lang For All Seasons (September 2015)

Presented at RacketCon 2015. [abstract]

Racket is a programming-language programming language. We used this power to build an extensible family of languages for checking poems for correctness. See here for the implementation.

Position Paper: Performance Evaluation for Gradual Type Systems (July 2015)

Presentation at STOP 2015 (co-located workshop at ECOOP 2015). Performance evaluation needs to be a priority for gradual type systems. We recommend measuring the performance of all configurations on example programs, and reporting the proportion of configurations with acceptable performance (for example, under 200% slowdown).

Materials and Shapes (December 2014)

The long story on materials and shapes; essentially Sections 2 and 3 of our PLDI 2014 paper. Presented to (and well-critiqued by) the Brown PL group.

Parametric Polymorphism through run-time sealing (September 2014)

This paper combines two very different worlds, Scheme and System F, and proves that the resulting multi-language system has something very much like parametricity. The only caveats are that mixed programs might diverge or raise exceptions -- that's all! Talk given to the Cornell PL club.

From Parametricity to Conservation Laws (April 2014)

Ben Carriel and I gave this presentation to the Cornell PL club. The original POPL 2014 paper by Robert Atkey is here. We included Dijkstra to wake up the audience for our main point: that viewing types as geometries helps give insight into when you can and can't extract a free theorem.

Full Reductions at Full Throttle (December 2013)

Talk given to the Cornell PL club. The original paper by Boespflug et al. can be found here. Slide 34 is the punch line, everything else is leading up to that clever/useful/frightening exploit.

Miscellaneous lecture notes here.