ICFP/SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
Thu 16 Oct 2025 14:45 - 15:30 at Peony NE - ML Workshop 2 Chair(s): Sam Westrick

This talk will introduce the CakeML project and some of the major milestones we have achieved since our last appearance at the ML Workshop in 2014. These include a new optimizing compiler backend, new language frontends, new tools for program verification, and new verified applications. I will give particular focus to recent applications of CakeML in verified proof checking. Here, CakeML-based tools offer state-of-the-art, end-to-end verified correctness guarantees for the automated reasoning community. Conversely, building verified proof checkers has highlighted pain points in CakeML’s tooling and workflows for end-to-end verified software, which we are working to address in ongoing work.

Thu 16 Oct

Displayed time zone: Perth change

13:45 - 15:30
ML Workshop 2ML Family Workshop at Peony NE
Chair(s): Sam Westrick New York University
13:45
30m
Talk
Freezing Bidirectional Typing (Extended Abstract)
ML Family Workshop
Wenhao Tang The University of Edinburgh, Shengyi Jiang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Sam Lindley University of Edinburgh
Pre-print
14:15
30m
Talk
A typed approach to ontology manipulation (experience report)
ML Family Workshop
Davide Camino University of Torino, Italy, Andrea Zito University of Torino, Italy, Viviana Bono University of Torino, Lorenzo Bafunno University of Torino, Italy, Lorenzo Pasini University of Torino, Italy, Emanuele Rovaretto University of Torino, Italy
14:45
45m
Talk
From CakeML to Proof Checking, and Back AgainInvited Talk
ML Family Workshop
Yong Kiam Tan Institute for Infocomm Research, A*STAR