Transitioning from Structural to Nominal Code with Efficient Gradual TypingIn-Person
Fri 22 Oct 2021 22:20 - 22:35 at Zurich D - Types & Verification -- mirror Chair(s): Atsushi Igarashi
Gradual typing is a principled means for mixing typed and untyped code.
But typed and untyped code often exhibit different programming patterns.
There is already substantial research investigating gradually giving types to code exhibiting typical untyped patterns, and some research investigating gradually removing types from code exhibiting typical typed patterns.
This paper investigates how to extend these established gradual-typing concepts to give formal guarantees not only about how to change types as code evolves but also about how to change such programming patterns as well.
In particular, we explore mixing untyped "structural" code with typed "nominal" code in an object-oriented language.
But whereas previous work only allowed "nominal" objects to be treated as "structural" objects, we also allow "structural" objects to dynamically acquire certain nominal types, namely interfaces.
We present a calculus that supports such "cross-paradigm" code migration and interoperation in a manner satisfying both the static and dynamic gradual guarantees, and demonstrate that the calculus can be implemented efficiently.
Fri 22 OctDisplayed time zone: Central Time (US & Canada) change
13:50 - 15:10 | Types & VerificationOOPSLA at Zurich D +8h Chair(s): Leonidas Lampropoulos University of Maryland, College Park | ||
13:50 15mTalk | Scalability and Precision by Combining Expressive Type Systems and Deductive VerificationVirtual OOPSLA Florian Lanzinger KIT, Alexander Weigl KIT, Mattias Ulbrich KIT, Werner Dietl University of Waterloo DOI | ||
14:05 15mTalk | A Type System for Extracting Functional Specifications from Memory-Safe Imperative ProgramsVirtual OOPSLA Paul He University of Pennsylvania, Edwin Westbrook Galois, Brent Carmer Galois, Chris Phifer Galois, Valentin Robert Galois, Karl Smeltzer Galois, Andrei Ştefănescu Galois, Aaron Tomb Galois, Adam Wick Galois, Matthew Yacavone Galois, Steve Zdancewic University of Pennsylvania DOI | ||
14:20 15mTalk | Transitioning from Structural to Nominal Code with Efficient Gradual TypingIn-Person OOPSLA DOI | ||
14:35 35mLive Q&A | Discussion, Questions and Answers OOPSLA |
21:50 - 23:10 | |||
21:50 15mTalk | Scalability and Precision by Combining Expressive Type Systems and Deductive VerificationVirtual OOPSLA Florian Lanzinger KIT, Alexander Weigl KIT, Mattias Ulbrich KIT, Werner Dietl University of Waterloo DOI | ||
22:05 15mTalk | A Type System for Extracting Functional Specifications from Memory-Safe Imperative ProgramsVirtual OOPSLA Paul He University of Pennsylvania, Edwin Westbrook Galois, Brent Carmer Galois, Chris Phifer Galois, Valentin Robert Galois, Karl Smeltzer Galois, Andrei Ştefănescu Galois, Aaron Tomb Galois, Adam Wick Galois, Matthew Yacavone Galois, Steve Zdancewic University of Pennsylvania DOI | ||
22:20 15mTalk | Transitioning from Structural to Nominal Code with Efficient Gradual TypingIn-Person OOPSLA DOI | ||
22:35 35mLive Q&A | Discussion, Questions and Answers OOPSLA |