Focusing on Refinement Typing - A Logically Principled Foundation

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.