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.
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.
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.
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.
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.
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.
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).
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.
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.
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.
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.
