Sophia Drossopoulou
Professor, Imperial College London
Sophia is Professor of Programming Languages at Imperial College London. She started her career in research in compilers, and in particular parsers and attribute grammars. But then she was drawn into the beautiful world of programming languages, and what can be expressed naturally and succinctly with the right choice of paradigm. Since then, she has been working on type systems, module systems, ownership types, traits, type-state and session types for oo languages, and concurrency. With her students, they were the first to propose gradual typing and type inference for Javascript. She is passionate about getting to the bottom of things, and formulating the most elegant and precise explanation.
Past Activities
Code Mesh V
17.10 - 18.10
Panel discussion: Types for All: From weak to strong, from static to dynamic
When working from home, everyone looked at what books were on display on the shelves in the background. Type systems seemed to be very much in vogue, often put there to be seen. In order to not loose momentum, we are planning a panel on Type Systems at Code Mesh! It will be lead by Felienne Hermans of Leiden University.
The idea is to discuss the panelists' approach to type systems, the rationale behind their design decisions, and how they have benefited the programming languages they have created. Questions will include, but not be limited to: when do we want type, when are types in the way, and what can we do about that? How extensible should a type system be? Attendees, through the Q&A section of the app, will be able to ask their own questions. With cameras on, don't forget to put your books on display.
Code Mesh LDN 2018
15.35 - 16.20
Towards specifications of robustness -- the things that programs do _not_ do
Programs are considered to be robust, if they behave “well” in all possible usage scenarios, whether intended or not. To help develop robust programs several programming language features and programming patterns have been proposed: constants, private members, encapsulation, capabilities, ownership, proxies, membranes etc. All these are powerful mechanisms which support the development of robust code.
However, these mechanisms do not address the question as to what specific guarantees we want the particular robust code to make. How do we express, eg, that a DOM-tree protected by a wrapper will not be modified beyond the part allowed by the wrapper, or that money will not disappear from a multiowner-account unless one of the account holders withdrew their money? Traditional program specifications, based on pre- and post- conditions do not address robustness either.
In this talk we will claim that robustness is about guaranteeing that certain thing will not happen – as opposed to functional specifications which are about what will happen. We will introduce "holistic specifications", an extension of traditional program specifications that support the expression of robustness properties through a logic with spatial and temporal features. We will show how holistic specifications can be used to specify robustness concerns in a number of popular program patterns from object-capabilities and smart contracts: the membrane, Mint-and-Purse, DOM-wrappers, the DAO, and ERC-20. We will show how to reason about the preservation of non-trivial properties concerning our data when it comes into contact with unknown, or adversarial code.
OBJECTIVES
To discuss what _is_ robustness, and how to specify robustness aspects of programs.