Preface

This volume contains the proceedings of the Ninth Workshop on Mathematically Structured Functional Programming (MSFP 2022), which took place on the 2nd of April as a satellite of European Joint Conferences on Theory & Practice of Software (ETAPS 2022).

The MSFP workshop highlights applications of mathematical structures to programming applications. We promote the use of category theory, type theory, and formal language semantics to the development of simple and reasonable programs. 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:

• Valeria de Paiva, Topos Institute, USA
  Going Without: A Linear Modality and its Role

• Nuria Brede, University of Potsdam, Germany
• Jacques Carette, McMaster University, Canada
• Youyou Cong, Tokyo Institute of Technology, Japan
• Philippa Cowderoy
• Jan de Muijnck-Hughes, University of Glasgow, UK
• Harley Eades III, Augusta University, USA
• Jeremy Gibbons (co-chair), University of Oxford, UK
• Jules Hedges, University of Stratchclyde, UK
• Shin-Ya Katsumata, National Institute of Informatics, Japan
• Max New (co-chair), University of Michigan, USA
• Maciej Piróg, University of Wrocław, Poland
• Artjoms Sinkarovs, Heriot-Watt University, UK

Jeremy Gibbons and Max S. New, April 2022

Going Without: A Linear Modality and its Role

Linear type theories have been with us for more than 25 years, from the beginning of Linear Logic, and they still have much to teach us. I want to discuss and compare four linear type theories and show how an overlooked system has much potential to help with open issues in modal type theory. We discuss the Linear Lambda Calculus (Benton et al), Plotkin and Barber's DILL (Dual Intuitionistic Linear Logic) and Benton's Linear-non-Linear (LNL) type theories. Then we recall how DILL can be transformed into ILT (Intuitionistic and Linear Type Theory), as described by Maietti et al 2000, a type theory without a modality, but with two functions spaces, and what we gain with this transformation. Finally, we speculate on how this transformation might be helpful for other modal type theories, their models and envisaged applications.