Projects per year
Abstract
C#, Dart, Pyret, Racket, TypeScript, VB: many recent languages integrate dynamic and static types via gradual typing. We systematically develop four calculi for gradual typing and the relations between them, building on and strengthening previous work. The calculi are as follows: λB, based on the blame calculus of Wadler and Findler (2009); λC, inspired by the coercion calculus of Henglein (1994); λS inspired by the spaceefficient calculus of Herman, Tomb, and Flanagan (2006); and λT based on the threesome calculus of Siek and Wadler (2010). While λB and λT are little changed from previous work, and λC are λS new. Together λB, λC, λS , λT , and provide a coherent foundation for design, implementation, and optimization of gradual types. We define translations from λB to λC, from λC to λS, and from λS to λT. 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 implementationready: the first spaceefficient calculus that is both straightforward to implement and easy to understand. We give two applications: first, using full abstraction from λC to λS to establish an equational theory of coercions; 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.
Original language  English 

Article number  e20 
Number of pages  56 
Journal  Journal of Functional Programming 
Volume  31 
DOIs  
Publication status  Published  13 Oct 2021 
Projects
 1 Finished

From Data Types to Session Types  A Basis for Concurrency and Distribution
20/05/13 → 19/11/20
Project: Research