No.103 Semantics of Effects, Resources, and Applications


NII Shonan Meeting Seminar 103

Abstracts of Lectures

Chung-Kil Hur – Relaxed Memory Models

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


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

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.


Category: Uncategorized


Comments are closed.