This program is tentative and subject to change.
Object-oriented programming languages typically allow mutation of objects, but pure methods are common too. There is great interest in recognizing which methods are pure, because it eases analysis of program behavior and allows modifying the program without changing its behavior. The roDOT calculus is a formal calculus extending DOT with reference mutability. In this paper, we explore purity conditions in roDOT and pose a SEF guarantee, by which the type system guarantees that methods of certain types are side-effect free. We use the idea from ReIm to detect pure methods by argument types. Applying this idea to roDOT required just a few changes to the type system, but necessitated re-working a significant part of the soundness proof. In addition, we state a transformation guarantee, which states that in a roDOT program, calls to SEF methods can be safely reordered without changing the outcome of the program. We proved type soundness of the updated roDOT calculus, using multiple layers of typing judgments. We proved the SEF guarantee by applying the Immutability guarantee, and the transformation guarantee by applying the SEF guarantee within a framework for reasoning about safe transformations of roDOT programs. All proofs are mechanized in Coq.
This program is tentative and subject to change.
Mon 16 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:00 | |||
13:30 15mTalk | Behavioral up/down casting for statically typed languages Technical Papers Lorenzo Bacchiani University of Bologna, Mario Bravetti Università di Bologna, Marco GIUNTI University of Oxford, João Mota NOVA School of Science and Technology, António Ravara Nova University of Lisbon | ||
13:45 15mTalk | Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency Technical Papers Farzaneh Derakhshan Illinois Institute of Technology, Stephanie Balzer Carnegie Mellon University, Yue Yao Carnegie Mellon University | ||
14:00 15mTalk | Ozone: Fully Out-of-Order Choreographies Technical Papers Dan Plyukhin University of Southern Denmark, Marco Peressotti University of Southern Denmark, Fabrizio Montesi University of Southern Denmark Pre-print | ||
14:15 15mTalk | Information Flow Control in Cyclic Process Networks Technical Papers Bas van den Heuvel Karlsruhe University of Applied Sciences, University of Freiburg, Farzaneh Derakhshan Illinois Institute of Technology, Stephanie Balzer Carnegie Mellon University | ||
14:30 15mTalk | Formalizing, Mechanizing, and Verifying Class-based Refinement Types Technical Papers Ke Sun Peking University, Di Wang Peking University, Sheng Chen UL Lafayette, Meng Wang University of Bristol, Dan Hao Peking University | ||
14:45 15mTalk | Pure methods for roDOT Technical Papers Vlastimil Dort Charles University, Yufeng Li University of Waterloo, Ondřej Lhoták University of Waterloo, Pavel Parizek Charles University |