YoVDO

Translating HOL-Light Proofs to Coq

Offered By: Hausdorff Center for Mathematics via YouTube

Tags

Formal Verification Courses Logic Courses Lambda Calculus Courses Type Theory Courses Coq Courses

Course Description

Overview

Save Big on Coursera Plus. 7,000+ courses at $160 off. Limited Time Only!
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

Verifying the LLVM
Strange Loop Conference via YouTube Beweisbar sichere Software
media.ccc.de via YouTube RustBelt: A Quick Dive Into the Abyss - Formalizing Rust's Safety Story
Rust via YouTube Building Measure Theory Using Hierarchy Builder
Hausdorff Center for Mathematics via YouTube Using Formal Methods to Eliminate Exploitable Bugs - YOW! 2015
GOTO Conferences via YouTube