MetaCoq - Verified Meta-Theory at Scale for a Certified Proof Assistant

Join a one-hour seminar presentation where Dr. Meven Lennon-Bertrand from the University of Cambridge explores MetaCoq, focusing on verified meta-theory at scale for certified proof assistants. Delivered as part of the Big Specification (BSP) series at the Isaac Newton Institute, learn about the latest developments in mathematical sciences and their applications across science and technology. Engage with cutting-edge research presented by one of the leading mathematical scientists, contributing to the institute's mission of fostering international research collaboration and mathematical innovation.