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

Displayed time zone: Tijuana, Baja California change

09:15 - 10:55
Semantics IIResearch Papers at PLDI Main RED (Portland 256)
Chair(s): Robby Findler Northwestern University
09:15
25m
Talk
Declarative Programming over Eventually Consistent Data Stores
Research Papers
KC Sivaramakrishnan University of Cambridge, Gowtham Kaki Purdue University, Suresh Jagannathan Purdue University
Media Attached
09:40
25m
Talk
Blame and coercion: Together again for the first time
Research Papers
Jeremy G. Siek Indiana University, Peter Thiemann University of Freiburg, Philip Wadler University of Edinburgh
Media Attached
10:05
25m
Talk
Lightweight, Flexible Object-Oriented Generics
Research Papers
Yizhou Zhang Cornell University, Andrew C. Myers , Barbara Liskov MIT, Guido Salvaneschi TU Darmstadt, Matt Loring Cornell University
Media Attached
10:30
25m
Talk
Relatively Complete Counterexamples for Higher-Order Programs
Research Papers
Phúc C. Nguyễn , David Van Horn University of Maryland, College Park
Media Attached