Published: 30th June 2022 DOI: 10.4204/EPTCS.360 ISSN: 2075-2180 |
Preface Jeremy Gibbons and Max S. New | |
Invited Talk: Going Without: A Linear Modality and its Role Valeria de Paiva | |
Combinatory Adjoints and Differentiation Martin Elsman, Fritz Henglein, Robin Kaarsgaard, Mikkel Kragh Mathiesen and Robert Schenck | 1 |
LibNDT: Towards a Formal Library on Spreadable Properties over Linked Nested Datatypes Mathieu Montin, Amélie Ledein and Catherine Dubois | 27 |
Tableless Calculation of Circular Functions on Dyadic Rationals Peter Kourzanov | 45 |
The Programming of Algebra Fritz Henglein, Robin Kaarsgaard and Mikkel Kragh Mathiesen | 71 |
Sikkel: Multimode Simple Type Theory as an Agda Library Joris Ceulemans, Andreas Nuyts and Dominique Devriese | 93 |
What Makes a Strong Monad? Dylan McDermott and Tarmo Uustalu | 113 |
On Structuring Functional Programs with Monoidal Profunctors Alexandre Garcia de Oliveira, Mauro Jaskelioff and Ana Cristina Vieira de Melo | 134 |
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:
Jeremy Gibbons and Max S. New, April 2022
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.