Gradual type theory
Abstract
Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. While existing gradual type soundness theorems for these languages aim to show that type-based reasoning is preserved when moving from the fully static setting to a gradual one, these theorems do not imply that correctness of type-based refactorings and optimizations is preserved. Establishing correctness of program transformations is technically difficult, because it requires reasoning about program equivalence, and is often neglected in the metatheory of gradual languages.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 02, 2019
- Source ID
- 10.1145/3290328
Entities
People
- Amal Ahmed
- Daniel R. Licata
- Max S. New
Organizations
- Air Force Research Laboratory
- National Science Foundation
- Northeastern University
- Wesleyan University