Emotion Oriented Systems 2022

Linear Logic

Aggregate Programming for the Internet of Things

With the ongoing explosion of data production and availability of devices with computational capabilities, traditional centralized data-processing techniques start to suffer from the increasing costs of data transfer, infrastructure, security and privacy needs. The edge/fog computing paradigm has emerged to meet these challenges, particularly for Internet of Things and open Cyber-Physical Systems. It processes data where it is generated in order to address the shortcomings of centralized techniques. However, decentralized architectures have their own challenges: handling device unreliability, data volatility, and coping with conficting goals. Aggregate Programming is a recent abstraction allowing one to program large-scale networks in a simple way, while providing strong guarantees on the resilience of the resulting behaviour under changes and unreliability. This abstraction shifts the local viewpoint of single device behaviour, to the global viewpoint of overall system behaviour; leaving the (automated) global-to-local translation to language implementation. This short course presents the Aggregate Programming abstraction, together with its commonly used distributed algorithms that have strong resilience guarantees, and its toolkit (programming language and simulator).

Foundations of communication-centred programming

In modelling distributed systems where processes interact by means of message passing, one soon realises that many interactions are meant to occur following disciplined protocols.

The ability to describe complex interaction protocols by means of a formal, simple and yet expressive type language can have a profound impact on the way distributed systems are designed and developed. This is witnessed by the fact that some important standardisation bodies for web-based business and finance protocols have recently investigated design and implementation frameworks for specifying message exchange rules and validating business logic based on the notion of sessions, where session types are “shared agreements” between teams of programmers developing possibly large and complex distributed protocols or software systems.

Aim of this course is to provide a gentle introduction to session type theory, enlightening aspects which are at the core of the current research in this subject.

The course material is available at http://www.di.unito.it/~dezani/papers/ohrid.pdf.

Formal methods and automatic reasoning in Agda

The course is aimed to introduce formal methods in computer science by means of tools based on type theory, especially AGDA. Lectures will concern the grounds of type theory, namely intuitionistic logic and lambda calculus, eventually focussing on dependent types and Martin-Loef intuitionistic type theory, of which AGDA is an implementation.

Applications to foundations of programming languages, program verification and language-based security are illustrated.

Quantum Computing 2021-22

Introduction to Deep Learning 2022

Deep learning based approaches outperform traditional approaches in a number of applications spanning from data analysis  to image processing and natural language processing. The availability of large sets of annotated data, powerful yet affordable parallel computers and improved optimization techniques are behind this revolution. This course will provide first an introduction to multilayer neural networks and its cornerstones such as learning with descent of the backpropagated error gradient. Next, convolutional and deep architectures will be introduced in the context of image processing, Finally, the course will look into recurrent architectures for time series and natural language processing.