SPLASH Workshop/Symposium Events 2025
2025 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH Events 2025)
Powered by
Conference Publishing Consulting

3rd ACM SIGPLAN International Workshop on Functional Software Architecture (FUNARCH 2025), October 12–18, 2025, Singapore, Singapore

FUNARCH 2025 – Proceedings

Contents - Abstracts - Authors

3rd ACM SIGPLAN International Workshop on Functional Software Architecture (FUNARCH 2025)

Frontmatter

Title Page


Welcome from the Chairs
Welcome to the third ACM SIGPLAN Workshop on Functional Software Architecture—Functional Programming in the Large (FUNARCH), in Singapore on October 12, co-located with ICFP 2025! This workshop was born out of the observation that the functional program- ming community has developed a great body of knowledge on how to develop software. Increasingly, industry is applying functional programming to great effect in large-scale projects. Unfortunately, very little is written up on how to do this in comprehensive form. Thus, adopters of functional programming in the large must rely on folklore and experience (or wading through decades of ICFP papers). This makes functional programming effectively inaccessible to many architects, developers, and projects. One goal of this workshop is to be part of a long-term effort to address this problem. Simultaneously, the software architecture community has developed a large body of useful knowledge, literature and pedagogy, largely untouched by func- tional programming. The two communities have much to learn from each other. Facilitating this cross-pollination is another goal of this workshop. Most of all, we hope to have a great day communicating and collaborating on our joint effort—developing great software functionally!

FUNARCH 2025 Organization


Papers

A Layered Certifying Compiler Architecture
Jacco O.G. Krijnen, Wouter Swierstra, Manuel Chakravarty, Joris Dral, and Gabriele Keller
(Utrecht University, Netherlands; Tweag, Netherlands; IOG, Netherlands; Well-Typed, Netherlands)
The formal verification of an optimising compiler for a realistic programming language is no small task. Most verification efforts develop the compiler and its correctness proof hand in hand. Unfortunately, this approach is less suitable for today’s constantly evolving community-developed open-source compilers and languages. This paper discusses an alternative approach to high-assurance compilers, where a separate certifier uses translation validation to assess and certify the correctness of each individual compiler run. It also demonstrates that an incremental, layered architecture for the certifier improves assurance step-by-step and may be developed largely independently from the constantly changing main compiler code base. This approach to compiler correctness is practical, as witnessed by the development of a certifier for the deployed, in-production compiler for the Plinth smart contract language. Furthermore, this paper demonstrates that the use of functional languages in the compiler and proof assistant has a clear benefit: it becomes straightforward to integrate the certifier as an additional check in the compiler itself, leveraging the the Rocq prover’s program extraction.

Publisher's Version
Six Years of FUNAR: Functional Training for Software Architects
Michael Sperber
(Active Group, Germany)
Since 2019, the International Software Architecture Qualification board has featured a three-day curriculum for Functional Software Architecture. We have taught more than 30 trainings based on this curriculum, mostly to audiences with little or no exposure to functional programming. This paper reports on our experience, and how content and delivery of the training has evolved over the past four years.

Publisher's Version
Evolution of Functional UI Paradigms
Michael Sperber and Markus Schlegel
(Active Group, Germany)
Functional paradigms for user-interface (UI) programming have undergone significant evolution, from early stream-based approaches, monad-based toolkits mimicking OO practice to modern model-view-update frameworks. Changing from the classic Model-View-Controller pattern to functional approaches drastically reduces coupling and improves maintainability and testability. On the other hand, achieving good modularity with functional approaches is an ongoing challenge. This paper traces the evolution of functional UI toolkits along with the architectural implications of their designs---including two of our own---summarizes the current state of the art and discusses remaining issues.

Publisher's Version

proc time: 0.74