COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |
University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > Tunable Static Inference for Generic Universe Types
Tunable Static Inference for Generic Universe TypesAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins. This event may be recorded and made available internally or externally via http://research.microsoft.com. Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending Object ownership is useful for many applications, including program verification, thread synchronization, and memory management. However, the annotation overhead of ownership type systems hampers their widespread application. This talk addresses this issue by presenting a tunable static type inference for Generic Universe Types. In contrast to classical type systems, ownership types have no single most general typing. Our inference chooses among the legal typings via heuristics. Our inference is tunable: users can indicate a preference for certain typings by adjusting the heuristics or by supplying partial annotations for the program. We present how the constraints of Generic Universe Types can be encoded as a boolean satisfiability (SAT) problem and how a weighted Max-SAT solver finds a correct Universe typing that optimizes the weights. We implemented the static inference tool, applied our inference tool to four real-world applications, and inferred interesting ownership structures. This talk is part of the Microsoft Research Cambridge, public talks series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsCentre for Smart Infrastructure & Construction NanoDTC Energy Materials Talks Science talksOther talksKnot Floer homology and algebraic methods Bayesian optimal design for Gaussian process model Political Thought, Time and History: An International Conference Title to be confirmed Planck Stars: theory and observations What sort of challenge is climate change? Fifty years of editorialising in ‘Nature’ and ‘Science’ A feast of languages: multilingualism in neuro-typical and atypical populations From Euler to Poincare BP KEYNOTE LECTURE: Importance of C-O Bond Activation for CO2/COUtilization - An Approach to Energy Conversion and Storage Immigration and Freedom "Mechanosensitive regulation of cancer epigenetics and pluripotency" A unifying theory of branching morphogenesis |