Mathematically Structured Functional Programming 2014

Mathematically Structured Functional Programming 2014

functionality from structure


The fifth workshop on Mathematically Structured Functional Programming is devoted to the derivation of functionality from structure. It is a celebration of the direct impact of Theoretical Computer Science on programs as we write them today. Modern programming languages, and in particular functional languages, support the direct expression of mathematical structures, equipping programmers with tools of remarkable power and abstraction. Where would Haskell be without monads? Functional reactive programming without arrows? Call-by-push-value without adjunctions? The list goes on. This workshop is a forum for researchers who seek to reflect mathematical phenomena in data and control.

Where and when?

MSFP 2014 will be held on 12 April. This time around, we're delighted to be affiliated with ETAPS 2014, running 5-13 April in Grenoble, France. Please register through ETAPS. The early rate registration deadline is Friday 14 February.

Our invited speakers are Bob Atkey and Shin-ya Katsumata, Kyoto University.


09:00-10:00 Invited talk
Applications of Relational Parametricity beyond Type Abstraction
Bob Atkey

Free Applicative Functors [pdf]
Paolo Capriotti and Ambrus Kaposi

10:30-11:00 Coffee

Monad transformers for backtracking search [pdf]
Jules Hedges

Normalization by Evaluation in the Delay Monad [pdf]
Andreas Abel and James Chapman

Coherence for skew-monoidal categories [pdf]
Tarmo Uustalu

12:30-14:00 Lunch

14:00-15:00 Invited talk
Logical Relations for Monads by Categorical TT-Lifting
Shin-ya Katsumata

Polymonadic Programming [pdf]
Michael Hicks, Gavin Bierman, Nataliya Guts, Daan Leijen and Nikhil Swamy

Koka: Programming with Row-polymorphic Effect Types [pdf]
Daan Leijen

16:00-16:30 Coffee

Categorical Semantics for Functional Reactive Programming with Temporal Recursion and Corecursion [pdf]
Wolfgang Jeltsch

Foundations of Total Functional Data-Flow Programming [pdf]
Baltasar Trancón Y Widemann and Markus Lepper

Abstracts of Invited Talks

Bob Atkey's talk
Applications of 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.

Shin-ya Katsumata's talk
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.


Submissions are welcomed on, but by no means restricted to, topics such as:


The proceedings will be published under the auspices of EPTCS with a Creative Commons license. Participants of the workshop will receive a print copy of the EPTCS volume.

We are using EasyChair to manage submissions. To submit a paper, please login here.

Papers must report previously unpublished work and not be submitted concurrently to another conference with refereed proceedings. Accepted papers must be presented at the workshop by one of the authors.

Papers must be prepared in LaTeX using the EPTCS macro package. There is no specific page limit but authors should strive for brevity.

Important dates

Abstract31 December 2013 (extended deadline)
Submission7 January 2014 (extended deadline)
Notification3 February 2014
Final version10 February 2014
Workshop12 April 2014

Programme Comittee

Previous MSFP Workshops

MSFP 2006

The inaugural MSFP Workshop was held in July 2006, in Kuressaare, Estonia, a fine curtain-raiser for MPC and AMAST. It was organized by Conor McBride and Tarmo Uustalu, and featured invited talks from John Power and Andrzej Filinski. The proceedings were published in the British Computer Society's "Electronic Workshops in Computing" Series, available here.

Revised selected papers (with a full re-refereeing process) have appeared as a special issue of the Journal of Functional Programming Volume 19 Issue 3-4.

MSFP 2008

The second MSFP Workshop was held in July 2008, at Reykjavik University, Iceland as part of ICALP 2008. It was organized by Conor McBride and Venanzio Capretta, and featured invited talks from Andrej Bauer and Dan Piponi. The proceedings were published in Electronic Notes in Theoretical Computer Science, v. 229, n. 5, available here.

MSFP 2010

The third MSFP Workshop was held in September 2010, in Baltimore, Maryland, before ICFP 2010. It was organized by Venanzio Capretta and James Chapman, and featured invited talks from Martín Escardó and Amy Felty. The proceedings were published by ACM Press, available here.

MSFP 2012

The fourth MSFP Workshop was held in March 2012, in Tallinn, Estonia, before ETAPS 2012. It was organized by James Chapman and Paul Levy, and featured invited talks from Danko Ilik and Neil Ghani. The proceedings were published by EPTCS, available here.

Last modified 16 September 2014 by Paul Levy