A Variation on Java Wildcards - Trading Expressiveness for Global Type Inference
This program is tentative and subject to change.
Java-TX is a dialect of Java with global type inference. To enable type inference, its treatment of wildcards is different from Java’s as Java-TX does not support capture conversion. Consequently, previous soundness proofs for Java with wildcards do not apply.
We introduce Featherweight Java-TX (FJ-TX), a functional core calculus for Java-TX which extends Featherweight Generic Java with wildcards. While previous models of wildcards rely on the standard encoding of wildcards by existential types, FJ-TX treats wildcards directly. Wildcard types in FJ-TX interact non-trivially with the instantiation of generics, which gives rise to a new kind of constraint.
We present the first type soundness proof for Java-TX, we discuss the ramifications of the different approaches to wildcards, and we offer a qualitative evaluation of these differences by examining the use of capture conversion in Java programs.
This program is tentative and subject to change.
Thu 2 JulDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
11:00 - 12:30 | |||
11:00 22mTalk | A Variation on Java Wildcards - Trading Expressiveness for Global Type Inference Technical Papers Andreas Stadelmeier DHBW Baden-Wuerttemberg Cooperative State University, Peter Thiemann University of Freiburg, Martin Plümicke DHBW Stuttgart, Campus Horb, Germany | ||
11:22 22mTalk | Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types Technical Papers | ||
11:45 22mTalk | Language-Integrated Recursive Queries Technical Papers Anna Herlihy EPFL, Amir Shaikhha University of Edinburgh, Anastasia Ailamaki EPFL, Martin Odersky EPFL | ||
12:07 22mTalk | NEST: Network Enforced Session Types Technical Papers Jens Kanstrup Larsen DTU, Alceste Scalas Technical University of Denmark, Guy Amir Hebrew University, Jules Jacobs Cornell University, Jana Wagemaker Radboud University, Nate Foster EPFL; Jane Street | ||