APLAS 2023
Sun 26 - Wed 29 November 2023 Taipei, Taiwan
Wed 29 Nov 2023 09:00 - 10:00 at Room 106 & 107, IIS - Keynote 3 Chair(s): Kazunori Ueda

The CakeML project has grown from its beginnings as a formally verified compiler for an ML-like language to a full ecosystem today capable of producing various end-to-end verified applications.

This talk will start with an introduction to CakeML, including its compiler’s novel verified bootstrapping process. Then, I will outline how the CakeML ecosystem can be used to build verified proof checking tools that are capable of efficiently scrutinizing the outputs of automated reasoning solvers. By developing these checkers in close collaboration with tool developers, CakeML can provide practical proof checking for various automated reasoning theories with a remarkably small and shared trusted base.

Wed 29 Nov

Displayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change

09:00 - 10:00
Keynote 3APLAS 2023 at Room 106 & 107, IIS
Chair(s): Kazunori Ueda Waseda University
Covering the Last Mile in Trustworthy Automated Reasoning with CakeML
APLAS 2023
Yong Kiam Tan Institute for Infocomm Research, A*STAR