[Pl-seminar] Reminder: 9/30: NUPRL Symposium Day: Jan Vitek, Michael Sperber and Ravi Chugh

[Vincent St-Amour]

NUPRL Seminar presents

Monday, 9/30
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)


Michael Sperber
Active Group

11:45 - 12:45

The purely functional fab

Modern semiconductor fabs pose a complex scheduling problem: A fab must
move an ever more diversified product mix through a big hall of very
expensive tools.  While doing that, it should keep delivery dates,
optimize throughput and minimize rejects.  Worse: As many of the tools
operate at the atomic level, a typical tool often breaks or operates
below spec.  Software can help manage this complexity, but needs to be
well-structured and predictable to be truly useful.  Traditional
imperative and relational techniques fail to solve some of the harder
problems in fab scheduling.  Functional programming is more efficient
for software development, but also brings additional advantages to the
table:

- Programming with compositional models enables systematically
  constructing domain models accessible to scheduling experts.

- Using persistent data structures ("purely functional programming")
  enables speculative simulation, which is needed to solve some complex
  scheduling problems.

- The use of algebra and structuring devices such as monads and arrows
  help structure parts of a scheduling system.

This talk describes our experience developing the ALPS system
("Advanced Logistics and Production System") together with Starview,
Inc.  As ALPS was developed concurrently with its implementation
language Star, the project offers some insights on programming
language design, particularly on the design of type systems.


Jan Vitek
Purdue University

2:30 - 3:30

Why JavaScript Programmers Hate You: an ode to dynamic languages

Formal approaches to program correctness through static software
verification have influenced the design of programming languages,
programming models, and developer tools for the last fifty years. Yet
static techniques can only handle a small fraction of the programs
written in the languages they claim to target. By and large academic
research in the field has been about analyzing languages that all look
and feel like Pascal; languages with a static type discipline and with
read-only programs. This has very little to do with popular languages in
use today. Languages like JavaScript, Python, Lua and R where typing is
dynamic and new behaviors can be synthesized at runtime through powerful
reflective programming interfaces. Instead of embracing dynamism and
trying to support popular programming idioms, our community keeps
proposing solutions that impose static disciplines on programmers. We
keep trying to find the inner Pascal in every JavaScript. This is bound
to drive practitioners away and ensure our continued irrelevance. Are we
bound to repeat history or is there a way out?


Ravi Chugh
University of California, San Diego

4:00 - 5:00

Nested Refinement Types for JavaScript

Decades of research on type systems have led to advances in the kinds of
programming features that can be reasoned about and the kinds of errors
that can be prevented. Nevertheless, the programming idioms in untyped,
or dynamic, languages make heavy use of features --- run-time type
tests, mutable objects indexed by dynamically computed keys, prototype
inheritance, and higher-order functions --- that are beyond the reach of
prior type systems.

In this talk, I will describe my dissertation work on Dependent
JavaScript (DJS), a statically typed dialect of the imperative,
object-oriented, dynamic language. To overcome the core challenges of
dynamic languages, DJS incorporates several new refinement type-based
techniques: nested refinement types, where the typing relation is
embedded into the logic in order to specify and verify types for objects
indexed by dynamic string keys; flow-sensitive refinement types to
retain the precision of refinements in the face of mutable variables;
and heap unrolling to precisely model the semantics of prototype
inheritance. The key characteristic of our techniques is to rely only on
decidable refinement logics, thus allowing DJS to use off-the-shelf SMT
solvers to help carry out expressive subtype checking. To demonstrate
how these novel techniques combine, I will describe the current
implementation of DJS and evaluate its expressiveness on a set of small,
but challenging, JavaScript examples adapted from several sources. I
will also identify several, I think, exciting directions of future work
that will build on DJS.