Siddhartha Prasad,
Ben Greenman,
Tim Nelson, and
Shriram Krishnamurthi
[pdf]
Model finders (such as Alloy and Forge) discover instances of a datatype specification
and counterexamples to conjectures.
Instances can help users debug their designs, but only if they are properly understood.
This paper introduces a visualizer called CnD that avoids misleading
diagrams by default and offers a low-code way to communicate domain-specific constraints.
CnD helps shed light on ``unknown unknowns'' in the early stages of a specification design.
Dibri Nsofor and
Ben Greenman
[pdf]
[bibtex]
[slides]
[blog post]
We are seeking the reason behind dynamic (any) types across thousands of
Python projects.
This paper begins with two hundred sample projects and presents:
the design of a corpus study, eight patterns of dynamic use, and plans to
identify the patterns automatically.
Ashton Wiersdorf,
Stephen Chang,
Matthias Felleisen, and
Ben Greenman
[pdf]
[bibtex]
[doi]
[artifact]
[blog post]
Type systems evolve too slowly to keep up with evolving
libraries. Type tailoring offers a lightweight solution: let end users
modify the elaboration of surface code into the internal
language of the typechecker.
This paper introduces type tailoring as a theme that has emerged across
programming languages, it analyzes the core technical dimensions that
make tailoring work, and it outlines a vision for first-class language
support.
Ben Greenman,
Siddhartha Prasad,
Antonio Di Stasio,
Shufang Zhu,
Giuseppe De Giacomo,
Shriram Krishnamurthi,
Marco Montali,
Tim Nelson, and
Milda Zizyte
[pdf]
[bibtex]
[doi]
[artifact]
[google drive]
[slides]
[img]
[blog post]
Instruments on Qualtrics:
[beginner]
[LTL]
[LTLf]
Instrument PDFs:
[beginner]
[LTL]
[LTLf]
With the growing use of temporal logics, it is critical that users have a
clear understanding of what a specification means.
We introduce two test instruments, a dataset of over 3,000 responses,
and a refined catalog of misconceptions that cover both infinite-trace
LTL and finite-trace LTLf.
The catalog is of interest to formula authors and maintainers, and to
tool builders, who can use it to identify mistakes.
The test instruments are suitable for classroom
teaching or self-study.
Tim Nelson,
Ben Greenman,
Siddhartha Prasad,
Tristan Dyer,
Ethan Bove,
Qianfan Chen,
Charles Cutting,
Thomas Del Vecchio,
Sidney LeVine,
Julianne Rudner,
Ben Ryjikov,
Alexander Varga,
Andrew Wagner,
Luke West, and
Shriram Krishnamurthi
[pdf]
[bibtex]
[doi]
[blog post]
Forge brings lightweight formal methods to experienced programmers.
It is deeply inspired by Alloy and has been refined through four semesters of teaching Forge.
The key additions are a gradual progression of languages,
a toolkit for domain-specific visualizations,
and a form of unit testing for logical predicates.
Siddhartha Prasad,
Ben Greenman,
Tim Nelson, and
Shriram Krishnamurthi
[pdf]
[bibtex]
[doi]
[blog post]
We gave students full, in-IDE access to GPT-3 during a course on system specification.
Did GPT make the course trivial? No.
In fact, students rarely used the extension.
They preferred to do their own work (!).
Our VSCode extension is available [link].
We hope other educators try similar experiments so that we can all learn how to best
use LLMs to improve classroom learning.
Ben Greenman,
Matthias Felleisen, and
Christos Dimoulas
[pdf]
[bibtex]
[artifact]
[v2 slides]
[v1 slides]
[code]
[youtube]
Can off-the-shelf profiling tools lead the way from a slow gradually-typed
program to a faster one, in a 3D type migration lattice?
For now, probably not!
We explored over 1 million configurations and the best-case strategy
succeeded in only 50% of scenarios and only when allowing two
performance regressions.
On the bright side, our large-scale simulation experiment shows that
the rational programmer method is useful beyond contracts and error
messages.
Special thanks to Cloudlab
for free single-user machines to collect data on.
Matthew Flatt,
Taylor Allred,
Nia Angle,
Stephen De Gabrielle,
Robert Bruce Findler,
Jack Firth,
Kiran Gopinathan,
Ben Greenman,
Siddhartha Kasivajhula,
Alex Knauth,
Jay McCarthy,
Sam Phillips,
Sorawee Porncharoenwase,
Jens Axel Søgaard, and
Sam Tobin-Hochstadt,
[pdf]
[bibtex]
[artifact]
Rhombus brings language-oriented programming out of the Lisp world
and into a normal (Python-like) syntax.
The key features that make it possible are:
Shrubbery notation, multiple spaces for expansion,
unified pattern languages,
and a protocol for static information.
Ben Greenman
[pdf]
[html]
[slides]
[bibtex]
[artifact]
The GTP Benchmark Suite combines practical programs, a domain-specific
experimental method, and software for reproducibility.
Since 2014 the benchmarks have supported research in gradual typing
performance and related topics including type migration and debugging.
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.
![[img]](../resources/img/ben/fm24.jpeg){kind=link}
![[art]](../resources/img/makinghay.png){kind=link}