Proof Theory Impressionism - Blurring the Curry-Howard Line
Offered By: Strange Loop Conference via YouTube
Course Description
Overview
Explore the intricacies of the Curry-Howard Correspondence in this 35-minute conference talk from Strange Loop. Delve into the relationship between logical propositions and programming language types, examining the challenges of bridging the gap between formal proofs and practical implementations. Discover potential approaches to infuse production languages like Rust and Haskell with capabilities typically found in provable systems. Investigate concepts such as totality, type-level programming, and dependent types, drawing connections between these explorations and proof assistant languages. Gain insights into addressing the challenges of ensuring faithful implementation of proofs in safety-critical system software, including avionics, medical devices, and autonomous vehicles.
Syllabus
"Proof Theory Impressionism: Blurring the Curry-Howard Line" by Dan Pittman
Taught by
Strange Loop Conference
Tags
Related Courses
Sniffing the MetaverseStrange Loop Conference via YouTube KalDB - A Cloud Native Log Search Platform
Strange Loop Conference via YouTube The Evolution of a Planetary-scale Distributed Database
Strange Loop Conference via YouTube Machine Learning for Developer Productivity
Strange Loop Conference via YouTube Formally Verifying Everybody's Cryptography
Strange Loop Conference via YouTube