ICFP 2021
Sun 22 - Sat 28 August 2021
Sun 22 Aug 2021 22:00 - 23:00 at TyDe - Keynote Chair(s): Hsiang-Shang ‘Josh’ Ko

Last year, I set out on a journey to automatically prove some properties about floating-point computations in a whole host of different proof assistants. Eventually, I ended up writing Schmitty, which integrates Agda with SMT-LIB. In this talk, I’ll give an overview of the problems you’ll face integrating your favourite proof assistant with an external solver, and how different proof assistants chose to resolve – or not resolve – them.

Sun 22 Aug

Displayed time zone: Seoul change

22:00 - 23:30
KeynoteTyDe at TyDe
Chair(s): Hsiang-Shang ‘Josh’ Ko Institute of Information Science, Academia Sinica
Integrating Agda with SMT-LIB – An incomplete list of pits I fell inTyDe Keynote
Wen Kokke University of Edinburgh