Precise Inference of Expressive Units of Measurement Types
summary
PUnits is a static unit-of-measurement system that proves sound in Coq, encodes units as boolean and integer variables, and solves whole-program constraints with MaxSMT. It offers three modes—modular type checking, whole-program inference, and annotation—with annotation inserting inferred types back into source. Evaluation finds 3 unit errors in Gasflow that JScience misses, detects the known Daikon bug, produces UNSAT on 3 projects (fixing two), reduces runtime/memory >10%, and reports mode overheads (type checking ×7, inference ×49, annotation slower still).
AI-written summary · about
chapters (15)
- 0:00Intro
- 0:15Why a Units of Measurement Type System?
- 3:07PUnits Workflow
- 3:24Modular Type Checking Workflow
- 4:09Whole-program Inference Workflow
- 4:57Whole-program Inference with Annotation Workflow
- 5:23PUnits Features
- 6:38Constraint & SMT Encodings
- 7:43Revisiting the Firefox Bug
- 9:22Evaluation
- 10:02What are the benefits and trade-offs of using PUnits vs. existing Java unit libraries?
- 10:57Can PUnits detect and prevent units-related errors in real-world projects?
- 11:52Is PUnits suitable to use in a real-world development environment?
- 12:35Related Work
- 12:58Conclusions
related talks
01h 31mImplementing Physical Units Library for C++
24mAn Intrinsically-typed Probabilistic Programming Language in Coq (Extended Abstr...
28mEta conversion for the unit type (is still not that simple)
20mVerified Density Compilation for a Probabilistic Programming Language
19mType Inference Logics
56mOn Type-Based Techniques for Program Manipulation
59mUnification Modulo Equational Theories in Languages with Binding Operators
33mSolving constraints during type inference