September 30, 2022
The central idea of proof assistants is to help humans complete proofs, which sets them apart from mere type checkers. We usually have to include good error messages, namespace management, library management, linter, formatter, etc., to turn a type-checker into a realistic proof assistant. All famous proof assistants are equipped with these features, but their implementations are usually tied to a particular proof assistant and must be re-implemented for a new one. Experimenting with new type theories is thus difficult because one either has to hack the sophisticated codebase of an existing popular system, or to suffer from a rudimentary type-checker. Based on our experience in a series of experimental proof assistants for cubical type theory, we started creating reusable components to help anyone build their proof assistants. I will discuss Yuujinchou, a library for namespaces, and also other libraries under active development.
About Favonia
Favonia is an assistant professor at the University of Minnesota. They received their Ph.D. in 2017 from Carnegie Mellon University. Their main research interest is the correctness of programs and mathematical proofs, and they are currently working on cubical type theory, program testing, and the development of new proof assistants.