Talks

Shallow Typed Racket (October 2020)

Presented at Racket Con 2020. [src]

Preview of a transient semantics for Typed Racket. The new Shallow Typed Racket uses the same type checker as the original Deep Typed Racket, but does less to enforce types at runtime. Shallow types are type sound when interacting with Deep or untyped code, but nothing more. Hope this makes types more accessible to more Racket programmers.

The Typed Racket Optimizer vs. Transient (November 2019)

Presented at the Fall 2019 PRL Offsite meeting. [src]

10-minute talk about the Typed Racket optimizer and the transformations that are incompatible with a semantics that does not guarantee full type soundness. In brief: the optimizer does 15 kinds of things, 2 are incompatible, 1 requires that typed functions check their input, and ~3 others may be unsound depending on details of the soundness guarantees.

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, Dénès, and Grégoire 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.