Preface

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:

• Fredrik Nordvall Forsberg
  Higher inductive types in Homotopy Type Theory: applications and theory

We are grateful to our programme committee:

• Zena Ariola, University of Oregon
• Robert Atkey, University of Strathclyde (co-chair)
• Ornela Dardha, University of Glasgow
• Helle Hvid Hansen, Delft University of Technology
• Chantal Keller, IUT d'Orsay
• Neelakantan Krishnaswami, University of Birmingham (co-chair)
• Nicolas Wu, University of Bristol

Robert Atkey and Neel Krishnaswami, March 2016.

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.