2018/03/15 by Paola Giannini, Giannini, Paola, Tim Richter +5
Computer Science · #Advanced Database Systems and Queries #FOS: Computer and information sciences #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.1803.05838
openalex publication_date 2018/03/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We introduce a type and effect system, for an imperative object calculus, which infers "sharing" possibly introduced by the evaluation of an expression, represented as an equivalence relation among its free variables. This direct representation of sharing effects at the syntactic level allows us to express in a natural way, and to generalize, widely-used notions in literature, notably "uniqueness" and "borrowing". Moreover, the calculus is "pure" in the sense that reduction is defined on language terms only, since they directly encode store. The advantage of this non-standard execution model with respect to a behaviourally equivalent standard model using a global auxiliary structure is that reachability relations among references are partly encoded by scoping.