Wed 17 Jun 2015 09:40 - 10:05 at PLDI Main RED (Portland 256) - Semantics II Chair(s): Robby Findler

C#, Dart, Pyret, Racket, TypeScript, VB: many recent languages integrate dynamic and static types via gradual typing. We systematically develop three calculi for gradual typing and the relations between them, building on and strengthening previous work. The calculi are: λB, based on the blame calculus of Wadler and Findler [2009]; λC, inspired by the coercion calculus of Henglein [1994]; λS inspired by the space-efficient calculus of Herman, Tomb, and Flanagan [2006] and the threesome calculus of Siek and Wadler [2010]. While λB is little changed from previous work, λC and λS are new. Together, λB, λC, and λS provide a coherent foundation for design, implementation, and optimisation of gradual types.

We define translations from λB to λC and from λC to λS. Much previous work lacked proofs of correctness or had weak correctness criteria; here we demonstrate the strongest correctness criterion one could hope for, that each of the translations is fully abstract. Each of the calculi reinforces the design of the others: λC has a particularly simple definition, and the subtle definition of blame safety for λB is justified by the simple definition of blame safety for λC. Our calculus λS is implementation-ready: the first space-efficient calculus that is both straightforward to implement and easy to understand. We give two applications: first, using full abstraction from λC to λS to validate the challenging part of full abstraction between λB and λC; and, second, using full abstraction from λB to λS to easily establish the Fundamental Property of Casts, which required a custom bisimulation and six lemmas in earlier work.

Wed 17 Jun

pldi2015-papers
09:15 - 10:55: Research Papers - Semantics II at PLDI Main RED (Portland 256)
Chair(s): Robby FindlerNorthwestern University
pldi2015-papers09:15 - 09:40
Talk
KC SivaramakrishnanUniversity of Cambridge, Gowtham KakiPurdue University, Suresh JagannathanPurdue University
Media Attached
pldi2015-papers09:40 - 10:05
Talk
Jeremy G. SiekIndiana University, Peter ThiemannUniversity of Freiburg, Philip WadlerUniversity of Edinburgh
Media Attached
pldi2015-papers10:05 - 10:30
Talk
Yizhou ZhangCornell University, Andrew Myers, Barbara LiskovMIT, Guido SalvaneschiTU Darmstadt, Matt LoringCornell University
Media Attached
pldi2015-papers10:30 - 10:55
Talk
Phúc C. Nguyễn, David Van HornUniversity of Maryland, College Park
Media Attached