My PhD advisor, Dr Shaowei Lin is giving a talk at the topos institute colloquium with the abstract of his talk below:

Abstract

The Curry-Howard correspondence between proofs and programs suggests that we can exploit proof assistants for writing software. I will discuss the challenges behind a naïve execution of this idea, and some preliminary strategies for overcoming them. As an example, we will organize higher-order information in knowledge graphs using dependent type theory, and automate the answering of queries using a proof assistant. In another example, we will explore how decentralized proof assistants can enable mathematicians or programmers to work collaboratively on a theorem or application. If time permits, I will outline connections to canonical structures, reflection (ssreflect), transport, unification and universe management.

In his talk, he briefly mentions our work, so if you are interested in hearing more, you can access his talk recording on Youtube. His slides can be found here.