FUNARCH '25: "A Layered Certifying Compiler ..."
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.
@InProceedings{FUNARCH25p1,
author = {Jacco O.G. Krijnen and Wouter Swierstra and Manuel Chakravarty and Joris Dral and Gabriele Keller},
title = {A Layered Certifying Compiler Architecture},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {1-20},
doi = {10.1145/3759163.3760427},
year = {2025},
}
Publisher's Version
FUNARCH '25: "A Layered Certifying Compiler ..."
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.
@InProceedings{FUNARCH25p1,
author = {Jacco O.G. Krijnen and Wouter Swierstra and Manuel Chakravarty and Joris Dral and Gabriele Keller},
title = {A Layered Certifying Compiler Architecture},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {1-20},
doi = {10.1145/3759163.3760427},
year = {2025},
}
Publisher's Version
FUNARCH '25: "A Layered Certifying Compiler ..."
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.
@InProceedings{FUNARCH25p1,
author = {Jacco O.G. Krijnen and Wouter Swierstra and Manuel Chakravarty and Joris Dral and Gabriele Keller},
title = {A Layered Certifying Compiler Architecture},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {1-20},
doi = {10.1145/3759163.3760427},
year = {2025},
}
Publisher's Version
FUNARCH '25: "A Layered Certifying Compiler ..."
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.
@InProceedings{FUNARCH25p1,
author = {Jacco O.G. Krijnen and Wouter Swierstra and Manuel Chakravarty and Joris Dral and Gabriele Keller},
title = {A Layered Certifying Compiler Architecture},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {1-20},
doi = {10.1145/3759163.3760427},
year = {2025},
}
Publisher's Version
FUNARCH '25: "Evolution of Functional UI ..."
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.
@InProceedings{FUNARCH25p27,
author = {Michael Sperber and Markus Schlegel},
title = {Evolution of Functional UI Paradigms},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {27-38},
doi = {10.1145/3759163.3760429},
year = {2025},
}
Publisher's Version
FUNARCH '25: "Six Years of FUNAR: Functional ..."
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.
@InProceedings{FUNARCH25p21,
author = {Michael Sperber},
title = {Six Years of FUNAR: Functional Training for Software Architects},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {21-26},
doi = {10.1145/3759163.3760428},
year = {2025},
}
Publisher's Version
FUNARCH '25: "Evolution of Functional UI ..."
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.
@InProceedings{FUNARCH25p27,
author = {Michael Sperber and Markus Schlegel},
title = {Evolution of Functional UI Paradigms},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {27-38},
doi = {10.1145/3759163.3760429},
year = {2025},
}
Publisher's Version
FUNARCH '25: "A Layered Certifying Compiler ..."
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.
@InProceedings{FUNARCH25p1,
author = {Jacco O.G. Krijnen and Wouter Swierstra and Manuel Chakravarty and Joris Dral and Gabriele Keller},
title = {A Layered Certifying Compiler Architecture},
booktitle = {Proc.\ FUNARCH},
publisher = {ACM},
pages = {1-20},
doi = {10.1145/3759163.3760427},
year = {2025},
}
Publisher's Version