“Functional Software Architecture” refers to methods of construction and structure of large and long-lived software projects that are implemented in functional languages and released to real users, typically in industry.
The goals for the workshop are:
To assemble a community interested in software architecture techniques and technologies specific to functional programming;
To identify, categorize, and document topics relevant to the field of functional software architecture;
To connect the functional programming community to the software architecture community to cross-pollinate between the two.
FUNARCH 2025 will be co-located with ICFP 2025 in Singapore on October 17th 2025.
News is available on Mastodon, Bluesky, and Twitter.
The CFP is open.
The CFL is open.
... TBD, will be linked to after the conference.
FUNARCH adheres to the SIGPLAN/ICFP Code of Conduct.
This years videos will be available as a YouTube playlist; just like last year's.
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 Plutus 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 proof assistant’s program extraction.
Functional paradigms for user-interface (UI) programming have undergone significant evolution over the years, from early stream-based approaches, monad-based toolkits mimicking OO practice to modern model-view-update frameworks. Changing from the inherently imperative classic Model-View-Controller pattern to functional approaches has significant architectural impact, drastically reducing coupling and improving 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.
Since 2019, the International Software Architecture Qualification board has featured a three-day curriculum for Functional Software Architecture as part of its Advanced Level certification program. 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.
Jeffrey Young (Epic Games)
Cristine Rizkallah (University of Melbourne)
Isabella Stilkerich (Schaeffler Technologies)
Ryan Scott (Galois)
Facundo Dominguez (Tweag)
J. Garrett Morris (University of Iowa)
Nada Amin (Harvard University)
Tom Ellis (Groq)
KC Sivaramakrishnan (IIT Madras and Tarides)
Hidehiko Masuhara (Institute of Science Tokyo)