Periodic Reporting for period 4 - Matryoshka (Fast Interactive Verification through Strong Higher-Order Automation)

Proof assistants are increasingly used to verify hardware and software and to formalize mathematics. However, despite the success stories, they remain very laborious to use. The situation has improved with the integration of first-order automatic theorem...