ICFP/SPLASH 2025 (series) / ML Family Workshop 2025 (series) / Higher-order, Typed, Inferred, Strict: ML Family Workshop 2025 / From CakeML to Proof Checking, and Back Again
From CakeML to Proof Checking, and Back AgainInvited Talk
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 OctDisplayed time zone: Perth change
Thu 16 Oct
Displayed time zone: Perth change
13:45 - 15:30 | |||
13:45 30mTalk | 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 30mTalk | 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 45mTalk | From CakeML to Proof Checking, and Back AgainInvited Talk ML Family Workshop Yong Kiam Tan Institute for Infocomm Research, A*STAR |