Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language
We present a type-based analysis ensuring memory safety and object protocol completion in the Java-like language Mungo. Objects are annotated with usages, typestates-like specifications of the admissible sequences of method calls. The analysis entwines usage checking, controlling the order in which methods are called, with a static check determining whether references may contain null values. It prevents null pointer dereferencing and memory leaks and ensures that the intended usage protocol of every object is respected and completed. Moreover, the type system admits an algorithm that infers the most general usage wrt. a simulation preorder that makes a class declaration well-typed. It has been implemented in the form of a type checker and a usage inference tool.
Mon 30 NovDisplayed time zone: Osaka, Sapporo, Tokyo change
17:30 - 19:30 | |||
17:30 30mTalk | Syntactically Restricting Bounded Polymorphism for Decidable Subtyping Research Papers Julian Mackay Victoria University of Wellington, Alex Potanin Victoria University of Wellington, Jonathan Aldrich Carnegie Mellon University, Lindsay Groves Victoria University of Wellington | ||
18:00 30mTalk | A New Refinement Type System for Automated nu-HFLZ Validity Checking Research Papers Hiroyuki Katsura The University of Tokyo, Naoki Iwayama University of Tokyo, Japan, Naoki Kobayashi University of Tokyo, Japan, Takeshi Tsukada Chiba University, Japan | ||
18:30 30mTalk | Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language Research Papers Mario Bravetti Università di Bologna, Adrian Francalanza University of Malta, Iaroslav Golovanov Department of Computer Science, Aalborg University, Hans Hüttel Department of Computer Science, Aalborg University, Mathias Steen Jakobsen Department of Computer Science, Aalborg University, Denmark, Mikkel Klinke Kettunen Department of Computer Science, Aalborg University, Denmark, António Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS | ||
19:00 30mTalk | Neural Networks, Secure by Construction: An Exploration of Refinement Types Research Papers Wen Kokke University of Edinburgh, Ekaterina Komendantskaya Heriot-Watt University, UK, Daniel Kienitz Heriot-Watt University, David Aspinall University of Edinburgh, Robert Atkey University of Strathclyde |