Substructural typestates

Filipe Militão, Jonathan Aldrich, Luís Caires

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Citations (Scopus)

Abstract

Finding simple, yet expressive, verification techniques to reason about both aliasing and mutable state has been a major challenge for static program verification. One such approach, of practical relevance, is centered around a lightweight typing discipline where types denote abstract object states, known as typestates. In this paper, we show how key typestate concepts can be precisely captured by a substructural type-and-effect system, exploiting ideas from linear and separation logic. Building on this foundation, we show how a small set of primitive concepts can be composed to express high-level idioms such as objects with multiple independent state dimensions, dynamic state tests, and behaviororiented usage protocols that enforce strong information hiding. By exploring the relationship between two mainstream modularity concepts, state abstraction and hiding, we also provide new insights on how they naturally fit together and complement one another. Technically, our results are based on a typed lambda calculus with mutable references, location-dependent types, and secondorder polymorphism. The soundness of our type system is shown through progress and preservation theorems. We also describe a prototype implementation of a type checker for our system, which is available on the web and can be used to experiment with the examples in the paper. Categories and Subject Descriptors D.3.3 [Programming Languages]: Abstract Data Types; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs.

Original languageEnglish
Title of host publicationPLPV 2014 - Proceedings of the 2014 ACM SIGPLAN Workshop on Programming Languages Meets Program Verification, Co-located with POPL 2014
PublisherAssociation for Computing Machinery
Pages15-26
Number of pages12
ISBN (Print)9781450325677
DOIs
Publication statusPublished - 2014
Event2014 8th ACM SIGPLAN Workshop on Programming Languages Meets Program Verification, PLPV 2014 - Co-located with POPL 2014 - San Diego, CA, United States
Duration: 21 Jan 201421 Jan 2014

Conference

Conference2014 8th ACM SIGPLAN Workshop on Programming Languages Meets Program Verification, PLPV 2014 - Co-located with POPL 2014
CountryUnited States
CitySan Diego, CA
Period21/01/1421/01/14

Keywords

  • Aliasing
  • Capabilities
  • Linearity
  • Typestate

Fingerprint Dive into the research topics of 'Substructural typestates'. Together they form a unique fingerprint.

Cite this