Abstract
Heap entities tend to contain complex references to each other. To manage this complexity, types which express shapes and hierarchies have been suggested. We survey type systems which describe such hierarchic shapes, how these types are used for reasoning about programs, and applications in concurrent programming.
Slides available fromslurp.doc.ic.ac.uk/pubs.html#esop06.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aldrich, J., Chambers, C.: Ownership domains: Separating aliasing policy from mechanism. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 1–25. Springer, Heidelberg (2004)
Aldrich, J., Kostadinov, V., Chambers, C.: Alias Annotations for Program Understanding. In: OOPSLA (November 2002)
Bacon, D.F., Strom, R.E., Tarafdar, A.: Guava: a dialect of Java without data races. In: OOPSLA (2000)
Banerjee, A., Naumann, D.A.: Ownership confinement ensures representation independence for object-oriented programs. In: JACM (2005)
Banerjee, A., Naumann, J.D.A.: State based ownership, renetrnace and encapsulation. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol. 3586, pp. 387–411. Springer, Heidelberg (2005)
Barnett, M., DeLine, R., Fähndrich, M., Rustan, K., Leino, M., Schulte, W.: Verification of Object-Oriented Programs with Invariants. Journal of Object Technology (2004)
Barnett, M., Naumann, D.A.: Freinds Need a Bit More: Maintaining Invariants Over Shared State. Mathematics of Program Construction (2004)
Bokowski, B., Vitek, J.: Confined Types. In: OOPSLA (1999)
Boyapati, C., Lee, R., Rinard, M.: Ownership Types for Safe Programming: Preventing Data Races and Deadlocks. In: OOPSLA (2002)
Boyapati, C., Liskov, B., Shrira, L.: Ownership Types for Object Encapsulation. In: POPL (2003)
Boyapati, C., Rinard, M.: A Parameterized Type System for Race-Free Java Programs. In: OOPSLA (2002)
Boyapati, C., Salcianu, A., Beebee, W., Rinard, M.: Ownership Types for Safe Region-Based Memory Management in Real-Time Java. In: PLDI (June 2003)
Cele, G., Stureborg, S.: Ownership Types in Practice. Technical Report TR-02-02, Stockholm University (2002)
Clarke, D., Drossopolou, S.: Ownership, Encapsulation and the Disjointness of Type and Effect. In: OOPSLA (2002)
Clarke, D., Potter, J., Noble, J.: Ownership Types for Flexible Alias Protection. In: OOPSLA (1998)
Clarke, D., Richmond, M., Noble, J.: Saving the world from bad beans: Deployment-time confinement checking. In: OOPSLA (2003)
Clarke, D., Wrigstad, T.: External Uniqueness is Unique Enough. In: Cardelli, L. (ed.) ECOOP 2003, vol. 2743. Springer, Heidelberg (2003)
Grothoff, C., Palsberg, J., Vitek, J.: Encapsulating Objects with Confined Types. In: OOPSLA (2001)
O’ Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL (2004)
Ishtiaq, S., O’ Hearn, P.W.: Bi as an assertion language for mutable data structures. In: POPL (2000)
M. Leino, K.R., Müller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004, vol. 3086, pp. 491–515. Springer, Heidelberg (2004)
Müller, P., Poetzsch-Heffter, A.: Universes: A Type System for Controlling Representation Exposure. In: Programming Languages and Fundamentals of Programming (1999)
Müller, P., Poetzsch-Heffter, A., Leavens, G.: Modular Invariants for Layered Object Structures. Technical Report 424, ETH Zürich (2004) (further development under way)
Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular Specification of Frame Properties in JML. In: Concurrency and Computation Practice and Experience (2003)
Noble, J.: Visualising Objects: Abstraction, Encapsulation, Aliasing and Ownership. In: Diehl, S. (ed.) Dagstuhl Seminar 2001. LNCS, vol. 2269, pp. 58–72. Springer, Heidelberg (2002)
Noble, J., Vitek, J., Potter, J.M.: Flexible alias protection. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol. 1445, p. 158. Springer, Heidelberg (1998)
Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL (2004)
Parnas, D.: On the Criteria to be Used in Decomposing Systems into Modules. Comm. ACS (1972)
Potanin, A., Noble, J.: Checking ownership and confinement properties. Formal Techniques for Java-like Programs (2002)
Potanin, A., Noble, J., Frean, M., Biddle, R.: Scale-free geometry in OO programs. Commun. ACM (2005)
Smith, M., Drossopoulou, S.: Cheaper Reasoning with Ownership Types. In: IWACO (2003)
Zhao, T., Noble, J., Vitek, J.: Scoped Types for Real-time Java. In: RTSS (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Drossopoulou, S., Clarke, D., Noble, J. (2006). Types for Hierarchic Shapes. In: Sestoft, P. (eds) Programming Languages and Systems. ESOP 2006. Lecture Notes in Computer Science, vol 3924. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11693024_1
Download citation
DOI: https://doi.org/10.1007/11693024_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33095-0
Online ISBN: 978-3-540-33096-7
eBook Packages: Computer ScienceComputer Science (R0)