We introduce two-sided type systems, which are a particular kind of sequent calculi for typing formulas. Two-sided type systems allow for hypothetical reasoning over the typing of compound program expressions, and the refutation of typing formulas. By incorporating a type of all values, these type systems support symmetrical notions of well-typing and ill-typing, guaranteeing both that well-typed programs don’t go wrong and that ill-typed programs do not evaluate - that is, reach a value. This makes two-sided type systems suitable for incorrectness reasoning in higher-order program verification, which we illustrate through an application to precise data-flow typing in a language with constructors and pattern matching. Finally, we investigate the internalisation of the meta-level negation in the system as a complement operator on types. This motivates an alternative semantics for the typing judgement, which guarantees that ill-typed programs don’t evaluate, but in which well-typed programs may yet go wrong.
Wed 17 JanDisplayed time zone: London change
10:30 - 11:50
|Generating Well-Typed Terms that are not "Useless"
|Indexed Types for a Statically Safe WebAssembly
Adam Geller Computer Science, University of British Columbia, Justin Frank University of Maryland, College Park, William J. Bowman University of British ColumbiaDOI Pre-print
|The Essence of Generalized Algebraic Data TypesRemote
|Ill-Typed Programs Don't Evaluate