Syntactic type soundness is too weak to tell apart different ways of running a program that mixes typed and untyped code. Complete monitoring is a stronger property that captures a meaningful distinction — a language satisfies complete monitoring iff it checks all interactions between typed and untyped code.

The literature on mixed-typed languages presents (at least) three fundamentally different ways of thinking about the integrity of programs that combine statically typed and dynamically typed code. Recently, we have been sorting them out.

This post explains the sampling method introduced in the paper On the Cost of Type-Tag Soundness

Last week, Northeastern hosted a PI meeting for the Gradual Typing Across the Spectrum NSF grant. The meeting was made of 20+ researchers from four institutions, and 12 technical talks. Schedule:

http://prl.ccs.neu.edu/gtp/pi2017/pi2017.html

A common thread among the talks was the question: how to convert a research idea into a tool for software developers?

Instead of being Pythonistas, Rubyists, or Racketeers we have to be scientists. — Matthias Felleisen

Yesterday we hosted a PI meeting for the Gradual Typing Across the Spectrum NSF grant, gathering researchers from a number of institutions who work on gradual typing (the meeting program can be found here). In case you aren’t familiar with gradual typing, the idea is to augment dynamically typed languages (think Python or Ruby) with static type annotations (as documentation, for debugging, or for tool support) that are guaranteed to be sound.

Gradual typing is these days a fairly popular area, but the research can seem fragmentary because of the need to support idiosyncratic language features. One of the points of the meeting was to encourage the cross-pollination of the key scientific ideas of gradual typing—the ideas that cross language and platform barriers.