Institute of Information Science, Academia Sinica

Proof assistants revolve around assisting humans in completing proofs, setting them apart from mere type checkers. To create a practical proof assistant, developers must incorporate components such as error reporting, namespace management, library management, linter, formatter, and more. While these features are present in well-known proof assistants, their implementations are tightly coupled with specific systems, requiring developers to re-implement them for new ones. As a result, experimenting with new type theories becomes arduous, as it necessitates either making complex modifications to existing codebases or settling for rudimentary type checkers. To tackle this challenge proactively, we draw from our experience with experimental proof assistants for cubical type theory and embark on creating reusable components that empower individuals to construct their own proof assistants. I will discuss Yuujinchou, a namespace library, and other actively-developed libraries.