Preface

This volume contains the proceedings of the Fifth Workshop on Mathematically Structured Functional Programming (MSFP 2014), taking place on 12 April, 2014 in Grenoble, France, as a satellite event of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014.

MSFP is devoted to the derivation of functionality from structure. It highlights concepts from algebra, semantics and type theory as they are increasingly reflected in programming practice, especially functional programming. As the range of papers presented in this year's workshop shows, this continues to be a fruitful interface.

We are honoured to host the following invited speakers:

• Robert Atkey

  Relational Parametricity beyond Type Abstraction

• Shin-ya Katsumata

  Logical Relations for Monads by Categorical TT-Lifting

We are grateful to our programme committee:

• Andreas Abel, Chalmers and Gothenburg University
• Neil Ghani, University of Strathclyde
• Makoto Hamana, Gunma University
• Neelakantan Krishnaswami (co-chair), University of Birmingham
• Paul Blain Levy (co-chair), University of Birmingham
• Rasmus Møgelberg, IT University of Copenhagen
• Russell O'Connor, Google Canada

and to Guillaume Allais, Fredrik Nordvall Forsberg, and Neil Sculthorpe for additional reviewing. We would also like to thank the ETAPS 2014 organizers, and the EPTCS staff.

Neel Krishnaswami and Paul Blain Levy, April 2014

Relational Parametricity beyond Type Abstraction

John Reynolds' theory of relational parametricity demonstrates that parametric polymorphic programs are invariant under change of data representation, a property that yields "free" theorems about programs just from their types. The range of applications of relational parametricity is dazzling: including data type representations, non-inhabitation results, and program optimisation.

I will talk about recent work that has extended Reynolds' theory beyond invariance under changes of data type representation to other kinds of invariants. Quantifying over geometrical transformations allows for free theorems for programs that manipulate geometric data, capturing geometric invariance properties. Likewise, quantifying over distances yields free theorems capturing continuity properties. The range of applications of generalised relational parametricity is equally promising: for example, geometric free theorems can be connected to classical mechanics and Noether's theorem to yield physical conservation laws directly from types.

Logical Relations for Monads by Categorical TT-Lifting

Logical relations are widely used to study various properties of typed lambda calculi. By extending them to the lambda calculus with monadic types, we can gain understanding of the properties on functional programming languages with computational effects. Among various constructions of logical relations for monads, I will talk about a categorical TT-lifting, which is a semantic analogue of Lindley and Stark's leapfrog method.

After reviewing some fundamental properties of the categorical TT-lifting, we apply it to the problem of relating two monadic semantics of a call-by-value functional programming language with computational effects. This kind of problem has been considered in various forms: for example, the relationship between monadic style and continuation passing style representations of call-by-value programs was studied around '90s. We give a set of sufficient conditions to solve the problem of relating two monadic semantics affirmatively. These conditions are applicable to a wide range of such problems. If time permits, I will also talk about a variant of this result, namely a generic soundness for the effect systems over effect monoids.