ICFP/SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore

This program is tentative and subject to change.

Sun 12 Oct 2025 11:00 - 11:45 at Seminar Room 8 - FUNARCH Talks #1 Chair(s): Jeffrey Young

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.

This program is tentative and subject to change.

Sun 12 Oct

Displayed time zone: Perth change

11:00 - 12:30
FUNARCH Talks #1FUNARCH at Seminar Room 8
Chair(s): Jeffrey Young Epic Games
11:00
45m
Talk
A Layered Certifying Compiler Architecture
FUNARCH
Jacco Krijnen Utrecht University, Wouter Swierstra Utrecht University, Netherlands, Manuel Chakravarty Tweag & IOG, Joris Dral Well-Typed, Gabriele Keller Utrecht University
11:45
45m
Talk
Evolution of Functional UI Paradigms
FUNARCH
Michael Sperber Active Group GmbH, Markus Schlegel Active Group GmbH