Write a Blog >>
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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

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