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 ; λC, inspired by the coercion calculus of Henglein ; λS inspired by the space-efficient calculus of Herman, Tomb, and Flanagan  and the threesome calculus of Siek and Wadler . 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 JunDisplayed time zone: Tijuana, Baja California change
09:15 - 10:55
|Declarative Programming over Eventually Consistent Data Stores|
KC Sivaramakrishnan University of Cambridge, Gowtham Kaki Purdue University, Suresh Jagannathan Purdue UniversityMedia Attached
|Blame and coercion: Together again for the first time|
Jeremy G. Siek Indiana University, Peter Thiemann University of Freiburg, Philip Wadler University of EdinburghMedia Attached
|Lightweight, Flexible Object-Oriented Generics|
Yizhou Zhang Cornell University, Andrew C. Myers , Barbara Liskov MIT, Guido Salvaneschi TU Darmstadt, Matt Loring Cornell UniversityMedia Attached
|Relatively Complete Counterexamples for Higher-Order Programs|
Research PapersMedia Attached