UNSOUND 2024
as the organisers put it
Sources of Unsoundness in Type Systems and Verification This workshop, which is in its second instance, is about all aspects of unsoundness in type system and verification tools and theories. It is meant to entertain a community-wide discussion on possible sources of unsoundness and how to avert, address, and tackle them. We are particularly interested in the presentation of previously unknown or lesser known problems as well as discussions of well-known soundness holes and how they affect the day-to-day of programming language researchers and users. Background Advanced static type systems ...
who it's for
programming language researchers, language designers, type system theorists, compiler engineers, verification tool developers, runtime and VM engineers, programming language students
topics
TypeScript mixin inheritance; coercive upcast proxies; method-local inner classes; erased generics visibility bug; dependent defunctionalization and refunctionalization; Type-in-Type axiom inconsistency; distributive subtyping over constructors; semantic subtyping and MLsub; content-addressable scraps language; address types with protocol timestamps; gradual abstract interpretation with checks
| title | author | length |
|---|---|---|
| The Inexact Superclass Problem | Bruno C. d. S. Oliveira | 41m |
Claims that TypeScript’s mixin pattern for first‑class classes and dynamic inheritance is type‑unsound, and demonstrates a concrete counterexample: a mixin… | ||
| Java Method-Local Inner Classes are Unsound | Marco Servetto, Nick Webster, Colin Gordon | 29m |
Claim: Java’s combination of method-local inner classes plus erased generics and class-based visibility lets a non-generic local class implicitly tied to a… | ||
| From FP to OOP and Back, Consistently | David Binder | 22m |
Extends dependent defunctionalization and refunctionalization to dependent types, proving the transformations are total and type-preserving and giving a… | ||
| On Distributive Subtyping with Finitary and Infinitary Unions and Intersections | Lionel Parreaux | 30m |
Argues that whether intersections and unions distribute over function and constructed types hinges on Church vs Curry divide: languages with internal typing… | ||
| Publishable Network Contracts in Scrapscript | Taylor Troesh | 34m |
A new language, Scrapscript, implements content-addressable scraps that are cryptographically signed and publishable to a “scrapyard” and an address type that… | ||
| Taming Unsoundness with Gradual Abstract Interpretation | Gaspar Ricci, Matías Toro, Sebastian Erdweg, Éric Tanter | 27m |
Proposes that optimistic but unsound assumptions in abstract interpretation become safe by automatically inserting runtime checks so analysis results are sound… | ||
| Welcome to UNSOUND | Lionel Parreaux | 19m |
Opens the UNSOUND workshop and defines unsoundness as a mismatch between claimed type guarantees and runtime behavior, then gives concrete examples and fixes… | ||
| nothing matches | ||