Programming languages, type systems, and logics have a long tradition
of wizardry. Experts conjure a language design and herald it to the
masses. The masses unsurprisingly tend to ignore the wizards, to the
detriment of both parties. This talk surveys methods to elevate the art
of language design toward a science of rigorous, well-grounded
measurements. Examples include corpus studies to discover typing
patterns and user surveys to reveal expert blind spots. Quite often,
insights from practitioners can lead to better languages.
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.
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.
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.
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.
Short talk about postdoc research: types to get programmers familiar with Alloy, quickly.
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!
Short talk about postdoc research: the context and the methods.
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.
