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
Programming LanguagesUniversity of Virginia via Udacity Compilers
Stanford University via Coursera Programming Languages, Part A
University of Washington via Coursera CSCI 1730 - Introduction to Programming Languages
Brown University via Independent Intro to Java Programming
San Jose State University via Udacity