No.103 Semantics of Effects, Resources, and Applications

Icon

NII Shonan Meeting Seminar 103

Sep 30, 2016 Comments Off on Overview

Overview

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 in the forms of effects and resources to make this abstraction effective and useful. The advantage of this approach is that program can be statically analyzed in order to verify that their behavior meet given specifications.

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.

Sep 30, 2016 Comments Off on Organizers

Organizers

  • Marco Gaboardi – gaboardi@buffalo.edu
    University at Buffalo, The State University of New York.
  • Shin-ya Katsumata – sinya@kurims.kyoto-u.ac.jp
    Research Institute for Mathematical Sciences, Kyoto University.

Sep 30, 2016 Comments Off on Lecturers

Lecturers

  • Chung-Kil Hur  – Seoul National University
  • Deepak Garg  – Max Planck Institute for Software Systems
  • Sam Lindley  – The University of Edinburgh
  • Paul-André Melliès – University Paris Diderot
  • Ulrich Schöpp – Ludwig-Maximilians-Universtät München
  • Niki Vazou – University of Maryland

Sep 30, 2016 Comments Off on Schedule

Schedule

  Sunday Monday Tuesday Wednesday Thursday Friday
7:30-9:00 breakfast breakfast breakfast breakfast breakfast
(check out)
9:00-10:30 Katsumata Schoepp Katsumata Garg Lindley
10:30-11:00 break break break break break
11:00-12:30 Mellies Hur Mellies Gaboardi Vazou
12:30-14:00 lunch lunch
picture 13:45		 lunch lunch lunch
14:00-15:30 Garg Lindley Excursion
13:25		 Schoepp leaving
15:30-16:00 check-in break break Excursion break
16:00-17:30 check-in Gaboardi Vazou Excursion Hur
18:30-20:00 check-in dinner dinner banquet dinner
20:00-22:00 banquet
(19:00)		 socializing socializing banquet socializing

Sep 30, 2016 Comments Off on Abstracts of Lectures

Abstracts of Lectures

Chung-Kil Hur – Relaxed Memory Models
gil-Shonan-pdf

In this lecture, I will talk about (i) relaxed memory behaviors occurring in modern compilers and multi-core hardware; (ii) problems with modelling such behaviors; and (iii) the state-of-the art models that tackle the problems.

Marco Gaboardi – Type System for Differential Privacy

Differential privacy is becoming a gold standard notion of privacy; it offers a guaranteed bound on loss of privacy due to release of query results, even under worst-case assumptions. In this lecture, I will introduce differential privacy and I will then present two methods based on two different type abstractions (a comonadic one, and a monadic one) that are useful for formally reasoning about differential privacy.

Deepak Garg – Relational effect analysis: Types and semantics

Traditional effect semantics define the observable effects of a single run of a program. However, many applications require analysis of the relative effects of the two runs of a program with two different inputs, or the runs of two similar programs. Such applications include information flow control, side-channel analysis in cryptography, stability analysis of algorithms and incremental computation. This lecture will cover types and semantic models (logical relations) for the analysis of relational effects.

Shin-ya Katsumata – Semantics of Effect Systems by Graded Monads
1st slide
2nd slide

Lucassen and Gifford’s effect system is a widely studied type-theoretic method to statically estimate program’s side effect. After Wadler’s seminal work on the unification of monadic types and effect annotations, the mathematical analysis of effect-annotated monadic types has been gradually emerged. In this lecture I will talk about one such analysis using graded monads. I first illustrate the concept of graded monad with examples, then present a denotational semantics of effect systems using graded monads.

Sam Lindley – Programming with algebraic effects and effect handlers

handlers
effdel

Links examples: links.tar.gz
Frank examples: frank.tar.gz

Plotkin and Pretnar’s handlers for algebraic effects support modular programming with effects. Algebraic effects define abstract interfaces for writing effectful programs and effect handlers are concrete implementations of such interfaces.

We introduce algebraic computations as computation trees and effect handlers as interpreters. We present effect handlers as a means for structured programming with delimited continuations. We exhibit examples ranging from the mathematical game of Nim to aspect-oriented programming to concurrent schedulers. These examples illustrate the modularity of effect handlers.

Paul-André Melliès – Resources and effects: a bifibrational approach

In these lectures, I will explain how to unify a number of fundamental concepts and tools related to resources and effects, using the mathematical notion of bifibration.

Ulrich Schöpp – Interaction Semantics and Programming Language Compilation
1st slide
2nd slide

Interaction semantics (Game Semantic, Geometry of Interaction) is an approach to programming language semantics that has produced precise models for many high-level languages. The central idea is to model program by simple dialogues between interacting entities. This idea can also give insight into the low-level implementation of high-level programming languages. If one lets low-level programs take the place of interactive entities, then semantic interpretation becomes low-level implementation. This lecture explains the organisation of low-level programs into interactive models, their structure, and how they can be used for the compilation of functional programming languages.

Niki Vazou – Liquid Types for Haskell
Webpage

Haskell’s type system allows developers to specify and verify a variety of program properties at compile time. However, many properties are impossible, or at the very least, cumbersome to encode within Haskell’s type system.

Liquid types enable the specification and verification of value-dependent properties by extending Haskell’s type system with logical predicates drawn from efficiently decidable logics.

In this talk, we present an overview of LiquidHaskell, a liquid type checker for Haskell. In particular, we will describe the kinds of properties that can be checked, ranging from generic requirements like totality and termination, to application specific concerns like memory safety, data structure correctness invariants, and effectfull computations.

 

Sep 30, 2016 Comments Off on Fees

Fees

The participation fee including full board, meeting fees and applicable taxes is 12,500 JPY per day.

  • Participants need to share a twin room (two participants per room).
  • Excursion fee, around 5,000 JPY, is not included in the participation fee.
  • NII Shonan School will NOT support travel for any participants.

We suggest students to bring their own personal computer at the School.

Category