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.