Write a Blog >>
Thu 21 Jan 2016 14:45 - 15:10 at Grand Bay South - Track 2: Types, Generally or Gradually Chair(s): Tiark Rompf

Language researchers and designers have extended a wide variety of type systems to support gradual typing, which enables languages to seamlessly combine dynamic and static checking. These efforts consistently demonstrate that designing a satisfactory gradual counterpart to a static type system is challenging, and this challenge only increases with the sophistication of the type system. Gradual type system designers need more formal tools to help them conceptualize, structure, and evaluate their designs. In this paper, we propose a new formal foundation for gradual typing, drawing on principles from abstract interpretation to give gradual types a semantics in terms of pre-existing static types. Abstracting Gradual Typing (AGT for short) yields a formal account of consistency—one of the cornerstones of the gradual typing approach—that subsumes existing notions of consistency, which were developed through intuition and ad hoc reasoning. Given a syntax-directed static typing judgment, the AGT approach induces a corresponding gradual typing judgment. Then the subject-reduction proof for the underlying static discipline induces a dynamic semantics for gradual programs defined over source-language typing derivations. The AGT approach does not recourse to an externally justified cast calculus: instead, run-time checks naturally arise by deducing evidence for consistent judgments during proof-reduction. To illustrate our approach, we develop novel gradually-typed counterparts for two languages: one with record subtyping and one with information-flow security types. Gradual languages designed with the AGT approach satisfy, by construction, the refined criteria for gradual typing set forth by Siek and colleagues.

Thu 21 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

14:20 - 16:00
Track 2: Types, Generally or GraduallyResearch Papers at Grand Bay South
Chair(s): Tiark Rompf Purdue & Oracle Labs
14:20
25m
Talk
Principal Type Inference for GADTs
Research Papers
Sheng Chen University of louisiana at Lafayette, Martin Erwig Oregon State University
Media Attached
14:45
25m
Talk
Abstracting Gradual Typing
Research Papers
Ronald Garcia University of British Columbia, Alison M. Clark , Éric Tanter University of Chile, Chile
Link to publication Media Attached
15:10
25m
Talk
The Gradualizer: a methodology and algorithm for generating gradual type systems
Research Papers
Matteo Cimini Indiana University, Jeremy G. Siek Indiana University
Media Attached
15:35
25m
Talk
Is Sound Gradual Typing Dead?
Research Papers
Asumu Takikawa Northeastern University, Daniel Feltey Northeastern University, Ben Greenman Northeastern University, Max S. New , Jan Vitek Northeastern University, Matthias Felleisen Northeastern University
Pre-print Media Attached File Attached