Published: 1st April 2016
DOI: 10.4204/EPTCS.207
ISSN: 2075-2180


Proceedings 6th Workshop on
Mathematically Structured Functional Programming
Eindhoven, Netherlands, 8th April 2016

Edited by: Robert Atkey and Neelakantan Krishnaswami

Robert Atkey and Neelakantan Krishnaswami
Invited Presentation: Higher inductive types in Homotopy Type Theory: applications and theory
Fredrik Nordvall Forsberg
Strong Typed Böhm Theorem and Functional Completeness on the Linear Lambda Calculus
Satoshi Matsuoka
Eilenberg–Moore Monoids and Backtracking Monad Transformers
Maciej Piróg
SMT Solving for Functional Programming over Infinite Structures
Bartek Klin and Michał Szynwelski
Variations on Noetherianness
Denis Firsov, Tarmo Uustalu and Niccolò Veltri
Directed Containers as Categories
Danel Ahman and Tarmo Uustalu


This volume contains the proceedings of the Sixth Workshop on Mathematically Structured Functional Programming (MSFP 2016), taking place on 8th April, 2016 in Eindhoven, Netherlands, as a satellite event of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016.

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 speaker:

We are grateful to our programme committee:

and to Fredrik Nordvall Forsberg for additional reviewing. We would also like to thank the ETAPS 2016 organizers, and the EPTCS staff.

Robert Atkey and Neel Krishnaswami, March 2016.

Higher inductive types in Homotopy Type Theory: applications and theory

Fredrik Nordvall Forsberg (University of Strathclyde)

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.