September 12, 2016
Svetlana Jakšić
Type systems are a widely used techniques for programming languages analysis. They are used to avoid undesired behaviours (run-time type errors), which are specific for each language. In this talk I will show how types can be used to avoid errors in two languages. The first language is modelling distributed network with RDF data. Even though such data is meant for public exposure and its availability brings a great advantage to users of such data, not all data are produced for public usage. For example, RDF is often used to represent personal information and data from social networks. This gives rise to the question of privacy of data, since the lack of privacy protection mechanisms often discourages people from publishing RDF data. A type system can be used to verify absence of some privacy violations. The second language is modelling a core language of processes that communicate and synchronize through the copyless message passing paradigm and can throw exceptions. In this context, where the sharing of data and explicit memory allocation require controlled policies on the ownership of heap-allocated objects, special care must be taken when exceptions are thrown to prevent communication errors (arising from misaligned states of channel endpoints) and memory leaks (resulting from messages forgotten in endpoint queues). We have studied a type system guaranteeing some safety properties, in particular that well-typed processes are free from communication errors and do no leak memory even in presence of (caught) exceptions. The talk is based on the results presented in my thesis.