In the context of gradual typing, type soundness guarantees the safety of typed
code. When untyped code fails to respect types, a runtime check finds the
discrepancy. As for untyped code, type soundness makes no promises; it
does not protect untyped code from mistakes in type specifications and
unwarranted blame.
To address the asymmetry, this paper adapts complete monitoring from the
contract world to gradual typing. Complete monitoring strengthens plain
soundness into a guarantee that catches problems with faulty type
specifications. Furthermore, a semantics that satisfies complete monitoring can
easily pinpoint the conflict between a type specification and a value. For
gradual typing systems that fail complete monitoring, the technical framework
provides a source-of-truth to assess the quality of blame.
Thu 24 Oct Times are displayed in time zone: Beirut change
16:00 - 16:22 Talk | Mergeable Replicated Data Types OOPSLA Gowtham KakiPurdue University, Swarn PriyaPurdue University, KC SivaramakrishnanIIT Madras, Suresh JagannathanPurdue University Link to publication DOI | ||
16:22 - 16:45 Talk | Refinement Kinds: Type-Safe Programming with Practical Type-Level Computation OOPSLA Luís CairesUniversidade Nova de Lisboa and NOVA LINCS, Bernardo ToninhoUniversidade Nova de Lisboa and NOVA LINCS DOI | ||
16:45 - 17:07 Talk | System FR: Formalized Foundations for the Stainless Verifier OOPSLA DOI | ||
17:07 - 17:30 Talk | Complete Monitors for Gradual Types OOPSLA Ben GreenmanPLT @ Northeastern University, Matthias FelleisenPLT @ Northeastern University, Christos DimoulasPLT @ Northwestern University DOI |