Relational Solver for Java Generics Type System
summary
Relational conversion of a Java subtyping verifier into a solver produces a tool that enumerates all substitutions for free type variables by combining a direct-subtyping relation and its reflexive-transitive closure, implemented in Min Canon and generated with no canon; performance improves via replacing Peano numbers with integers, ground-based closure selection and dynamic class-table search, and evaluation on a real-world class table of 40,000 classes with nine benchmark queries shows order-of-magnitude speedups and duplicate-answer elimination.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:05Motivation for Java solver
- 3:36Relational programming
- 5:26Inverse computation
- 7:34Solving type inequalities
- 8:16Direct subtyping implementation
- 9:46Transitive closure
- 10:08Performance optimizations
- 13:01Evaluation with class tables
- 17:14Summary and future work
- 18:42Question and answer session
related talks
14mRelational Synthesis for Pattern Matching
29mUnification Modulo Isomorphisms between Dependent Types for Type-based Library Search
24mAll for one and none forall: Compiling polymorphic relations without(…)
15mThe Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Ma...
26mCommitting to the bit: Relational programming with semiring arrays and SAT solving
16mMulti-stage Relational Programming
33mSolving constraints during type inference
26mtypedKanren: Statically Typed Relational Programming with Exhaustive Matching in(…)