Date and time: 16.08.2018 14:15-15:00

Speaker: Paola Giannini

Title: A type and effect system for uniqueness and immutability

Place: C114

Slides [PDF]


We define a type and effect system for expressing “uniqueness” and
“immutability” properties in imperative OO languages. The distinguishing
feature is that typechecking “infers” sharing possibly introduced by
the evaluation of an expression. In this way, expressions get very
expressive types: notably, uniqueness and immutability properties can
be detected from the fact that no sharing is introduced with the final
result of the expression. Sharing is directly represented at the syntactic
level as a relation among free variables, and a block construct allow us
to mantain in the runtime environment the underlying structure of the
code, thanks to the fact that the underlying calculus is “pure”. That is,
imperative features are modeled by just rewriting source code terms.

Paola Giannini got her undergraduate degree from the University of Pisa and her Master of Science in Computer Science from Carnegie-Mellon University of Pittsburg. She was Research Associate at the Computer Science Department of the University of Torino, and is now Full Professor of Computer Science at the University of Piemonte Orientale. Her research’s interests cover the area of semantic and logic of programming and, in particular, type systems for static analysis and semantic specification of functional, object oriented, and dynamic/scripting languages. Moreover, recently she started working on in the area of behavioural types an in particular on multiparty session types. She is author of over 70 papers in conferences and journals, has served as Program Committee member of conferences and workshops, as advisor of several Ph.D students, and has been site coordinator of some Italian and European projects. She has been also in charge of the undergraduate program in Computer Science for several years.