Translating HOL-Light Proofs to Coq
Offered By: Hausdorff Center for Mathematics via YouTube
Course Description
Overview
Explore the process of translating HOL-Light proofs to Coq in this informative 29-minute talk by Frédéric Blanqui from the Hausdorff Center for Mathematics. Gain insights into the challenges and techniques involved in bridging these two theorem proving systems, and learn about the practical applications of such translations. Discover the details of the project by accessing the associated GitHub repository at https://github.com/deducteam/hol2dk, which provides additional resources and code for those interested in delving deeper into this topic.
Syllabus
Frédéric Blanqui: Translating HOL-Light proofs to Coq
Taught by
Hausdorff Center for Mathematics
Related Courses
Programming Languages ⅠKorea Advanced Institute of Science and Technology via Coursera Meaning Representation for Natural Language Understanding - Mariana Romanyshyn - ODSC Europe 2019
Open Data Science via YouTube Propositions as Types
Strange Loop Conference via YouTube The Road to Akka Cluster, and Beyond
Strange Loop Conference via YouTube Making a Computer Turing Complete
Ben Eater via YouTube