The aim with Matryoshka, a five-year project starting in January 2017, is to design higher-order superposition provers and higher-order SMT solvers, and to integrate them in various proof assistants. I believe that reasonably strong higher-order reasoning is the crucial ingredient missing in today's automatic theorem provers to make them work very smoothly in the context of proof assistants. The goal is not to design new provers from scratch, but to build efficient higher-order provers on top of existing first-order provers, following a modular "Russian doll" architecture similar to that of SMT solvers.

CoCon is a conference management system with verified document confidentiality. What makes CoCon special compared to other conference systems is that it is built around a verified core that is guaranteed not to leak. Leakage of course refers to undesired information flow only. In general, a conference system is all about facilitating information flow: authors upload papers for committee members to read and discuss, committee members upload reviews and notifications for authors, etc. However, some information should remain partially or totally secret from some parties.

In principle all the major libraries of formalized mathematics can be translated into a formal system with a strong enough foundation, e.g., higher-order Tarski-Grothendieck set theory. In practice this is not so simple. The system MetaMath has a database of over 28,000 theorems of first-order Tarski-Grothendieck set theory. I will report on attempts to translate this MetaMath database to a Curry-Howard style proof checker for higher-order Tarski-Grothendieck set theory.