Explicit Refinement Types - A Type Theory with Embedded Proofs
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
Explore a groundbreaking presentation from the ICFP 2023 conference on Explicit Refinement Types. Delve into the innovative λert type theory, which introduces refinement types with explicit proofs. Learn how this system empowers programmers to embed property proofs directly into program text, supporting a rich logic including quantifiers and induction. Discover the advantages of this approach over traditional SMT solver-based systems like DML and Liquid Haskell. Examine the soundness of the type system through erasure to simply-typed programs and denotational semantics. Gain insights into the formalized proofs developed in Lean 4. Presented by Jad Elkhaleq Ghalayini and Neel Krishnaswami from the University of Cambridge, this 29-minute video offers a deep dive into advanced concepts in refinement types, first-order logic, and denotational semantics.
Syllabus
[ICFP'23] Explicit Refinement Types
Taught by
ACM SIGPLAN
Related Courses
Reverse Engineering 3201: Symbolic AnalysisOpenSecurityTraining2 via Independent Logic Against Sneak Obfuscated Malware
NorthSec via YouTube SMT- Quantifiers, and Future Prospects - IPAM at UCLA
Institute for Pure & Applied Mathematics (IPAM) via YouTube SMT Solvers in IT Security - Deobfuscating Binary Code with Logic
Cooper via YouTube Jumping the Fence - Comparison and Improvements for Existing Jump Oriented Programming Tools
YouTube