ECOOP 2025
Mon 30 June - Fri 4 July 2025 Bergen, Norway
Tue 1 Jul 2025 10:45 - 11:06 at Auditorium M003 - Type Systems and Program Semantics Chair(s): Sukyoung Ryu

We propose mono types, a new abstraction for programming Datalog. Mono types behave like first-class containers that can be stored in relations and to which elements can be added decentrally. But, mono types are more than just containers: They provide a read operation that can yield any result as long as it monotonically grows with each added element and is independent of the order in which elements are added to the container. This design permits a wide range of mono types (e.g., sets, maps, and aggregations), yet guarantees mono types can be integrated into Datalog without jeopardizing Datalog’s least fixed-point semantics. We develop a theory for mono types, which includes constructions for complex mono types, equivalence relation for mono types, and properties about semantics-preserving mono-type transformations. This theory ensures sound Datalog integration and justifies crucial compiler optimizations for mono types. Together, these techniques demonstrate that mono types provide abstraction without regret: We demonstrate in two case studies that programs become easier to write with mono types, while their performance also improves drastically.

Tue 1 Jul

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:45 - 12:30
Type Systems and Program SemanticsTechnical Papers at Auditorium M003
Chair(s): Sukyoung Ryu KAIST
10:45
21m
Talk
Mono Types — First-Class Containers for Datalog
Technical Papers
Runqing Xu JGU Mainz, David Klopp JGU Mainz, Sebastian Erdweg JGU Mainz
11:06
21m
Talk
Monadic type-and-effect soundness
Technical Papers
Francesco Dagnino University of Genoa, Paola Giannini University of Eastern Piedmont, Elena Zucca University of Genoa
11:27
21m
Talk
An Effectful Object Calculus
Technical Papers
Francesco Dagnino University of Genoa, Paola Giannini University of Eastern Piedmont, Elena Zucca University of Genoa
11:48
21m
Talk
Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness
Technical Papers
Pedro Carrott Imperial College London, Sacha-Élie Ayoun Imperial College London, Azalea Raad Imperial College London
DOI
12:09
21m
Talk
Practical Type-Based Taint Checking and InferenceRemote
Technical Papers
Nima Karimipour University of California, Riverside, Kanak Das University of California, Riverside, Manu Sridharan University of California at Riverside, Behnaz Hassanshahi Oracle Labs, Australia
:
:
:
: