How Profilers Can Help Navigate Type Migration (November 2023)

Presented at the BYU Grad Seminar Series.

Little Tricky Logics (March 2023)

Presented at LTLf @ AAAI-SSS'23.

We made an LTLf survey, delivered it to participants at the AAAI Spring Symposium on the Effectiveness of Temporal Logic on Finite Traces, and gave a brief summary of the results.

Shallow and Optional Types for Typed Racket (October 2022)

Presented at RacketCon 2022.

Typed Racket (TR) is powerful. It includes a type checker, a type-driven optimizer, and a contract layer that dynamically monitors interactions with untyped code. The contracts make TR one of the strongest and most flexible type systems in the world, but also one of the slowest when there are many boundaries to untyped. Shallow TR and Optional TR are two alternatives that weaken the types and improve performance at boundaries.

Fun and Games III: Summary of the Summer of #lang (October 2022)

Presented at RacketCon 2022.

Come learn about the amazing entries to this summer's #lang party! Submissions include new languages, improved languages, language ideas, and Standard ML.

Little Tricky Logic: Misconceptions in the Understanding of LTL (October 2022)

Presented at NJPLS @ UMD.

An interactive talk demonstrating specific ways that LTL formulas can be tricky. The findings are based on studies conducted over the past two years with a variety of learners. This work is a first step toward improved LTL tools and less-tricky temporal logics.

CIFellows Check-In: Typed Froglet (September 2022)

Short talk about postdoc research: types to get programmers familiar with Alloy, quickly.

Little Tricky Logic: Misconceptions in the Understanding of LTL (August 2022)

Presented at VardiFest. [extended abstract] [youtube]

It may be folk knowledge that LTL is tricky, but is it really, and if so in what ways and what can we do about it? This interactive talk demonstrates specific issues in the understanding of LTL and offers next steps for future work.
Given in celebration of Moshe Vardi's seminal contributions to LTL in particular and formal methods in general. Thanks Moshe!

Mixing Typed and Untyped Code: A Tale of Proofs, Performance, and People (Spring 2022)

Faculty job talk.

CIFellows Check-In: Human Factors for Gradual Typing (February 2022)

Short talk about postdoc research: the context and the methods.

Fun and Games 2 (November 2021)

Presented at Racket Con 2021. [youtube] [src]

Debrief on the 2021 Syntax Parse Bee.
Original entries: github.com/syntax-objects/Summer2021.
Syntax Parse Examples: docs.racket-lang.org/syntax-parse-example.

Shallow Typed Racket (October 2020)

Presented at Racket Con 2020. [youtube] [live QA] [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.