Dependent refinement types allow Typed Racket programmers to express rich type relationships, ranging from data structure invariants such as red-black tree balance to preconditions such as vector bounds. Refinements allow programmers to embed the propositions that occurrence typing in Typed Racket already reasons about into their types. Further, extending occurrence typing to refinements allows us to make the underlying formalism simpler and more powerful.
In addition to presenting the design of our system, we present a formal model of the system, show how to integrate it with theories over both linear arithmetic and bitvectors, and evaluate the system in the context of the full Typed Racket implementation. Specifically, we take safe vector access as a case study, and examine all vector accesses in a 56,000 line corpus of Typed Racket programs. Our system is able to prove that 50% of these are safe with no new annotation, and with a few annotations and modifications, we can capture close to 80%.
Thu 16 JunDisplayed time zone: Tijuana, Baja California change
10:30 - 12:00
|Accepting Blame for Safe Tunneled Exceptions|
Yizhou Zhang Cornell University, Guido Salvaneschi TU Darmstadt, Quinn Beightol Cornell, Barbara Liskov MIT, Andrew Myers Cornell UniversityLink to publication DOI Media Attached
|Occurrence Typing Modulo Theories|
Research PapersPre-print Media Attached
|Refinement Types for TypeScript|
Panagiotis Vekris University of California, San Diego, Benjamin Cosman University of California, San Diego, Ranjit Jhala University of California, San DiegoMedia Attached