This program is tentative and subject to change.

Sun 20 Oct 2024 16:00 - 16:30 at Pasadena - OOP

Finding a combination of types and static checks that guarantees some desired property such as type soundness (programms don’t get stuck) or consistency (not all types are inhabitated) is not enough. These checks should also be stable under those transformations that we perform when we write code. In “Deriving Dependently-Typed OOP from First Principles” that I will present at OOPSLA ’24, we extend the defunctionalization and refunctionalization transformations to dependent types, show that they are type preserving, and prove that the resulting system is sound. One of our major motivations is to allow programmers to switch between a functional design using data types and an object-oriented, interface-based design using codata types. However, the paper contains one major caveat: The system is not consistent since it doesn’t check for strict positivity of data and codata type declarations, uses the Type-in-Type axiom, and allows arbitrary mutual recursion. The reason we do not implement these checks is that although the defunctionalization and refunctionalization algorithms are semantics-preserving, the corresponding static checks are not preserved. For example, a program containing only strictly positive type declarations might be changed into a program in which type declarations contain negative recursive occurrances. This problem motivates the research problem that I am going to present: We want to find a way to check for the consistency of programs which is stable under defunctionalization and refunctionalization.

Extended Abstract (abstract.pdf)28KiB

This program is tentative and subject to change.

Sun 20 Oct

Displayed time zone: Pacific Time (US & Canada) change

16:00 - 17:30
16:00
30m
Talk
From FP to OOP and Back, Consistently
UNSOUND
David Binder University of Tübingen
File Attached
16:30
30m
Talk
Java Method-Local Inner Classes are Unsound
UNSOUND
Marco Servetto VUW, Nick Webster Victoria University of Wellington , Colin Gordon Drexel University
17:00
30m
Talk
The Inexact Superclass ProblemOnline
UNSOUND
Bruno C. d. S. Oliveira University of Hong Kong