arXiv:1604.00384v1 [cs.PL] 1 Apr 2016
DOI:
10.4204/EPTCS.207 ISSN: 2075-2180 |
Preface 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 | 1 |
Eilenberg–Moore Monoids and Backtracking Monad Transformers Maciej Piróg | 23 |
SMT Solving for Functional Programming over Infinite Structures Bartek Klin and Michał Szynwelski | 57 |
Variations on Noetherianness Denis Firsov, Tarmo Uustalu and Niccolò Veltri | 76 |
Directed Containers as Categories Danel Ahman and Tarmo Uustalu | 89 |
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:
Robert Atkey and Neel Krishnaswami, March 2016.
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.