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.
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.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.
Abstract | 31 December 2013 (extended deadline) |
Submission | 7 January 2014 (extended deadline) |
Notification | 3 February 2014 |
Final version | 10 February 2014 |
Workshop | 12 April 2014 |
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.
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.
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.
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