Ill-Typed Programs Don't Evaluate - Two-Sided Type Systems for Program Verification

Explore a groundbreaking approach to type systems in programming languages through this conference talk from POPL'24. Delve into the concept of two-sided type systems, a novel form of sequent calculi for typing formulas. Discover how these systems enable hypothetical reasoning over compound program expressions and refutation of typing formulas. Learn about the incorporation of a type for all values, leading to symmetrical notions of well-typing and ill-typing. Understand the guarantees provided by this approach, ensuring that well-typed programs don't go wrong and ill-typed programs do not evaluate. Examine the application of two-sided type systems in incorrectness reasoning for higher-order program verification, with a focus on precise data-flow typing in languages featuring constructors and pattern matching. Investigate the internalization of meta-level negation as a complement operator on types, and consider an alternative semantics for typing judgments that maintains the guarantee for ill-typed programs while allowing potential errors in well-typed programs.

Introduction
Type Theory
Sequin Calculi
Necessity Function Type
Soundness