Latte: Lightweight Aliasing Tracking for Java
summary
A formal alias-tracking type system for Java that requires annotations only on parameters and fields, infers all local aliases, and enforces unique parameters and owned parameters on the heap to allow safe destructive reads without runtime changes. The work is a formalism (no tool yet) that consumes unique values on use, mandates separate uniqueness across distinct parameters, and emits precise blame when merges or aliases fail—simpler and more IDE-friendly than ownership logics but intentionally less expressive.
AI-written summary · about
chapters (21)
- 0:00LATTE project introduction
- 0:42Motivation for alias tracking
- 2:50System goals and constraints
- 5:21Accommodating existing Java
- 7:11Related work comparison
- 10:00LATTE approach and annotations
- 13:18Stack implementation demo
- 15:27Isolation process details
- 17:37Stack tail access example
- 18:39Separate uniqueness requirement
- 20:05Value consumption and modality
- 21:28Merging environments in conditionals
- 23:14System goals recap
- 25:00Evaluation and future work
- 26:47Q&A
- 27:30Immutability parameter discussion
- 28:12Sound reasoning clarification
- 29:16Liquid types integration
- 29:40Java generics interaction
- 30:23Owned parameter escape
- 31:06Topology limitations
related talks
33mLatte: Lightweight Aliasing Tracking for Java
25mLiquidJava:Catch Bugs at Compile Time with Liquid Types
01h 00mJava Language Futures - All Aboard Project Amber
38mThe Sincerest Form of Flattery
23mThe Java Features You’re Missing Out On
29mHow (Not) To Write Java Pointer Analyses After 2020
44mJava for AI
44mIt’s Java, but Not As We Know It