Complete First-Order Reasoning for Properties of Functional Programs - OOPSLA 2023
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
Explore a 19-minute conference talk from OOPSLA2 2023 that delves into the theoretical foundations of automatic verification for functional programs. Uncover the generalization and formalization of heuristics used in tools like Liquid Haskell and Leon, revealing their completeness for reasoning with combined First-Order theories of algebraic datatypes and background theories. Gain insights into the efficacy of these heuristics, understand their limitations, and learn about the crucial role of user assistance in successful proofs. Presented by researchers from the University of Illinois at Urbana-Champaign and the University of California at San Diego, this talk covers topics such as First-Order Logic, completeness, refinement types, algebraic datatypes, and natural proofs, offering a comprehensive look at the theoretical underpinnings of functional program verification.
Syllabus
[OOPSLA23] Complete First-Order Reasoning for Properties of Functional Programs
Taught by
ACM SIGPLAN
Related Courses
Language, Proof and LogicStanford University via edX Artificial Intelligence: Knowledge Representation And Reasoning
Indian Institute of Technology Madras via Swayam AI:Knowledge Representation and Reasoning
Indian Institute of Technology Madras via Swayam 人工智慧:搜尋方法與邏輯推論 (Artificial Intelligence - Search & Logic)
National Taiwan University via Coursera Semantics of First-Order Logic
Stanford University via edX