Ben Greenman,
Christos Dimoulas, and
Matthias Felleisen
[pdf]
[bibtex]
[supplement]
The literature presents many strategies
for enforcing the integrity of types when typed code interacts with untyped code.
This paper presents a uniform evaluation framework that characterizes the
differences among some major existing semantics for typed--untyped interaction.
Type system designers can use this framework to analyze the guarantees of their own dynamic semantics.
Kuang-Chen Lu,
Ben Greenman, and
Shriram Krishnamurthi
[pdf]
[supplement]
[bibtex]
[src]
The Brown Benchmark for Table Types (B2T2) provides a focus for research on
type systems for tabular programming via five components:
(1) a definition of tables;
(2) a set of example datasets;
(3) an API of tabular operations with detailed type constraints;
(4) a set of short programs that use the table operations, each of which raises specific typing questions; and
(5) a set of buggy programs with explanations that describe the exact bug in the program.
Ben Greenman,
Lukas Lazarek,
Christos Dimoulas, and
Matthias Felleisen
[pdf]
[bibtex]
[slides]
[youtube]
[private src]
This paper reports on the surprising difficulties of adapting the Transient
semantics of Reticulated Python to the rich migratory type system of Typed
Racket. The resulting implementation, Shallow Typed Racket, is faster than the
standard Deep Typed Racket but only when the Transient blame assignment strategy is disabled.
For language designers, this report provides valuable hints on how to equip an existing
compiler to support a Transient semantics.
For theoreticians, the negative experience with Transient blame calls for
a thorough investigation of this strategy.
Ben Greenman
[pdf]
[bibtex]
[slides]
[youtube]
[src]
[NEU DRS pdf]
[ProQuest]
Presents four contributions:
(1) a systematic method to evaluate the performance of a mixed-typed language;
(2) formal properties that measure the strength of types;
(3) a scaled-up Transient semantics; and
(4) the design and implementation of a language that combines Deep types (complete monitoring), Shallow types (type soundness), and untyped code.
The combination helps avoid many worst-of-both-worlds situations
that arise with Deep types only or Shallow types only.
Ben Greenman,
Matthias Felleisen, and
Christos Dimoulas
[pdf]
[supplement]
[bibtex]
[slides]
[youtube]
[src]
Adapts complete monitoring into a (syntactic, operational) proof
technique for migratory typing.
A semantics satisfies complete monitoring iff it protects all channels
of communication between typed and untyped code.
Introduces blame soundness and blame completeness to
test whether systems that fail complete monitoring can identify
exactly the codes responsible for a run-time type mismatch.
Ben Greenman and
Matthias Felleisen
[pdf]
[supplement]
[bibtex]
[slides]
[youtube]
[src]
[redex models]
[artifact]
Compares the theory, performance, and implications (for a programmer)
of three approaches to adding types to a dynamically-typed language.
Update 2019-11-13: as it turns out, the paper describes a complete spectrum in ye olde "data processing" sense
(Kelly-Bootle, Stan. The Devil's DP Dictionary. McGraw-Hill Inc. 1981).
spectrum n. plural spectrums; mandatory DP usage wide spectrum(s). [Latin spectrum "an apparition."]
Any range of one or two items or features.
† A range of from three to seven features (the legal maximum) is known as a complete or total spectrum.
Ranges of eight or more are called unfair trading.
Miscellaneous lecture notes here.
![[art]](../resources/img/makinghay.png){kind=link}