Tue 20 Jun 2017 14:20 - 14:55 at Vertex WS217 - C Chair(s): Martin Berger

We introduce a type and effect system, for an imperative object calculus, which infers \emph{sharing} possibly introduced by the evaluation of an expression. Sharing is directly represented at the syntactic level as a relation among free variables, thanks to the fact that the calculus is \emph{pure}. That is, imperative features are modeled by just rewriting source code terms. We consider both standard variables and \emph{affine} variables, which can occur at most once in their scope. The latter are used as {temporary} references, to move'' a \emph{capsule} (an isolated portion of store) to another location in the store. The sharing effects inferred by the type system are very expressive, and generalize notions introduced in literature by type modifiers.

#### Tue 20 Jun

 14:00 - 15:30: FTfJP 2017 - C at Vertex WS217 Chair(s): Martin Berger 14:00 - 14:20Talk Generic Approach to Certified Static Checking of Module-like ConstructsJulia BelyakovaSouthern Federal University Pre-print 14:20 - 14:55Talk Tracing sharing in an imperative pure calculusPaola GianniniUniversita' del Piemonte Orientale, Marco ServettoVictoria University of Wellington, Elena ZuccaUniversity of Genova 14:55 - 15:30Talk Mutable WadlerFest DOTMarianna RapoportUniversity of Waterloo, Ondřej LhotákUniversity of Waterloo, Canada