Automating the Meta-Theory of Proof Systems

Proving properties about proof systems is a necessary task to make sure that they are sound and satisfy basic criteria for the application being considered. Nevertheless, it is a tedious and error-prone task. This project aims to develop a trustworthy system that helps with the verification of properties of proof systems. This system will allow for a natural specification of proof calculi and visualization of rules as close as possible to what one would write on paper. Moreover, it will provide proof objects for the properties of the specified proof systems, so that they can be checked independently. By freeing researchers from the hurdle of writing down big and repetitive proofs, we expect to facilitate the use of formal methods as a matter of course. This contributes to the reduction of errors and development of safer and more reliable systems. As an emerging country investing in modern technologies, it is in Qatar’s interest to ensure the correctness of automation to avoid errors and accidents.