1 Motivation Programs are dynamic entities that interact with their environment in a complex way. Understanding and controlling this behaviour is one of the central themes in programming language research. Several approaches have been proposed with the aim of representing the behavior of a program as some abstract mathematical structure that is manageable to program analysis. Formal semantics has provided the needed tools to make this abstraction effective and useful. The advantage of this approach is that program can then be statically analyzed in order to verify that their behavior meet given specifications. One such approach that has been particularly successful is the one based on the use of types for representing specifications and of type-checking and type-inference as program analyses guaranteeing that the programs respect these specifications. The success of this approach is also due to the strong connections between functional programming languages, logic, semantics and mathematics, represented by Curry-Howard isomorphism. The technological advancement in type systems has brought in recent years new tools that are useful to reason in an abstract way about non-functional aspects of program behavior such as side effects and resource consumption. Side effects, such as such as I/O, store updates, using randomness, and performing nondeterministic choice, are fundamental components of modern programming languages. The side effects caused by programs can be understood and controlled by using type systems that contain additional information useful to describe them. Type systems of this kind are often referred as effect systems. Effect systems are commonly used as framework to statically estimate program’s side effects and to enforce particular management policies for them. An interesting aspect of this approach is that effect systems can be directly relates to a rigorous representation of various side effects as monads, a concept from category theory. Resource consumption is another fundamental aspect of program’s behaviour. Several techniques have been proposed to describe resources in programs semantics. A technique that have found numerous applications in resource analysis is Linear Logic. Its key idea is to distinguish reusable (non-linear) data from single-use (linear) data using a comonad, another concept from category theory. This approach can be generalized to explicitly track different kind of data usage such as execution time, memory space, information flows, etc. Crucially, the approach proposed by linear logic can be easily integrated in type systems, providing new techniques for the analysis of resource usage of programs. Moreover, this approach has generated several important results in research areas where the notion of resource is a key component, such as implicit computational complexity, and sensitivity analysis in the context of differential privacy. The semantics understanding of effects and resources has also permitted the integration of these refined aspects of the programs behavior in the formal reasoning about practical applications. As an example, notions of resources and effect are now widely used when reasoning about the correctness of compilation and implementation of programs. Similarly, semantics models for resources and effects are used to reason about randomized algorithms.

2 Lectures The goal of the school is to share the cutting-edge techniques and various research problems in the semantic study of effects and resources in programming languages. To achieve this goal, we invite internationally recognized researcher, with excellent record of contributions in this area, to deliver lectures on their research.  We aim for a balance between theoretical lectures introducing the students to the mathematical structure of effects and resources (lectures by Melli`es, Katsumata and Sch¨opp) and more practical lectures introducing the students to the use of effects and resources in different applications (by Garg, Gaboardi, Hur, Lindley and Vazou).  These lectures may also include hands-on sessions to familiarize with the presented tools. The school program is designed to provide a broad range of topics: category theoretic framework for effects and resources (Melli`es, Katsumata), programming language implementation via geometry of interaction (Sch¨opp), type theory for reasoning about effects in a relational way (Garg) and in real-world programming languages (Lindley, Vazou), relaxed memory models (Hur), and probabilistic computation (Gaboardi). As attendees of the school we target PhD students, talented MSc students, and postdocs who are working in semantics, type systems and logic for programming languages, denotational semantics, program analysis, and their applications.

3 Expected output of the school We expect students to engage with other students and with the lecturers and organizers on different research topics. To enhance the interactions we will plan time for short students presentations early on in the school. This will help students and lecturers to identify other participants with similar interests. We will also require every lecturer to produce lecture notes which will be provided to students during the school. The lecture notes will also be collected in the school report that we will make publicly available to a broader audience.