Focusing on Refinement Typing - A Logically Principled Foundation
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
Explore a logically principled foundation for systematizing SMT constraint generation in refinement type systems for functional programming languages. Delve into a 19-minute conference talk that presents a novel approach combining a focalized variant of call-by-push-value, bidirectional typing, and value-determined indexes. Learn how this system generates solvable SMT constraints without existential variables, applicable to any computational effect and evaluation order. Examine the polarized subtyping relation that enables a sound, complete, and decidable logically focused typing algorithm. Discover how type soundness is proven using an elementary domain-theoretic denotational semantics, leading to total correctness and logical consistency. Gain insights into how the proof-theoretic technique of focalization simplifies both algorithmic and semantic results in this cutting-edge research presented at POPL'24.
Syllabus
[POPL'24] Focusing on Refinement Typing (TOPLAS)
Taught by
ACM SIGPLAN
Related Courses
Language, Proof and LogicStanford University via edX Proof Theory Impressionism - Blurring the Curry-Howard Line
Strange Loop Conference via YouTube Topics in Pure Model Theory - Lecture 10
Fields Institute via YouTube David Cerna: Proof Schema and the Refutational Complexity of Their Cut Structure
Hausdorff Center for Mathematics via YouTube Graham Leigh: On the Computational Content of Classical Sequent Calculus
Hausdorff Center for Mathematics via YouTube