Functionality from Structure
The sixth 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.
The proceedings have now been published as EPTCS Volume 207.
MSFP 2016 was held on Friday 8th April. This time around, we're delighted to be affiliated with ETAPS 2016, running 2nd-8th April in Eindhoven, The Netherlands.
We are delighted to have Fredrik Nordvall-Forsberg as our invited speaker this year. The title and abstract of Fred's talk are:
Higher inductive types in Homotopy Type Theory: applications and theory
Homotopy Type Theory is an foundational system and programming language that connects ideas from type theory and homotopy theory: we think of types as spaces, terms as points in a space, and of Martin-Löf's identity type as the path space of a given space. This led Lumsdaine and Shulman to consider a generalisation of inductive types, where not only points are freely generated, but also paths, paths between paths, and so on. Inductive types with such higher-dimensional generators are called Higher Inductive Types (HITs). HITs generalise ordinary inductive types, as well as quotient types, but also geometrical objects such as intervals, spheres or tori can be represented using HITs, leading the way to synthetic homotopy theory.
In this talk, I will give a gentle introduction to HITs. I will survey some of their applications, such as doing homotopy theory inside Homotopy Type Theory. I will then talk about the surprisingly relatively undeveloped theory underlying HITs. While we know many particular examples of HITs, we do not yet have a general schema for well-behaved definitions. Moreover, even for simple, "well-understood" HITs, we do not have proof-theoretical results such as normalisation or confluence. Trying to rectify this is joint work with Thorsten Altenkirch, Paolo Capriotti and Gabe Dijkstra.
The following papers were accepted for presentation at the workshop. The paper titles link to the published copies as part of the EPTCS proceedings.
Maciej Piróg. Eilenberg-Moore Monoids and Backtracking Monad Transformers.
Bartek Klin and Michał Szynwelski. SMT solving for functional programming over infinite structures.
Niccolò Veltri, Tarmo Uustalu and Denis Firsov. Variations on Noetherianness.
Danel Ahman and Tarmo Uustalu. Directed containers as categories.
Satoshi Matsuoka. Strong Typed Bohm Theorem and Functional Completeness on the Linear Lambda Calculus.
Day: Friday 8th April, 2016
09.30-10.30: Fredrik Nordvall-Forsberg: Higher inductive types in Homotopy Type Theory: applications and theory
break
11.00-11.45: Satoshi Matsuoka. Strong Typed Bohm Theorem and Functional Completeness on the Linear Lambda Calculus
11.45-12:30: Maciej Piróg, Eilenberg-Moore Monoids and Backtracking Monad Transformers
lunch
14.00-14.45: Bartek Klin and Michał Szynwelski. SMT solving for functional programming over infinite structures
14.45-15.30: Niccolò Veltri, Tarmo Uustalu, and Denis Firsov. Variations on Noetherianness
break
16.00-16.45: Danel Ahman and Tarmo Uustalu. Directed containers as categories
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.
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) 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.
The fifth MSFP Workshop was held in April 2014, in Grenoble, France, just after ETAPS 2014. It was organised by Neelakantan Krishnaswami and Paul Blain Levy, and featured invited talks from Robert Atkey and Shin-ya Katsumata. The proceedings were published by EPTCS, available here.