Operational Semantics driving the Type System Design: Reference Capabilities in Pony
The Pony programming language supports the actor paradigm, and allows sharing of mutable state in a data-race free manner. Data-race freedom is guaranteed through its novel type system based on reference capabilities, which determine how each actor may use the reference (read, write, immutable, isolated etc). In this talk we will show how the operational semantics drives the design of the type system, an insight which we obtained while deep in the design phase, and which lead to a more elegant and more powerful type system. If time permits, we will also outline how the type system is employed for fully concurrent Garbage Collection.
Sophia Drossopoulou is a Professor at Imperial College London, working on Programming Languages, Program Verification and Specification, and Object Capabilities. She is optimistic in her belief that most things have simple reasons, and is passionate about finding and formulating the most elegant, succinct and precise explanations.
I am a Professor of Programming Languages in the Department of Computing, Imperial College, London, UK.
Tue 16 JulDisplayed time zone: Belfast change
15:30 - 17:00
Summer School T3Summer School at Reims
|Operational Semantics driving the Type System Design: Reference Capabilities in Pony|
Sophia Drossopoulou Imperial College London