Ill-Typed Programs Don't Evaluate
Steven Ramsay, Charlie Walpole

TL;DR
This paper introduces two-sided type systems that enable reasoning about program correctness by ensuring well-typed programs don't go wrong and ill-typed programs don't evaluate, enhancing higher-order program verification.
Contribution
It presents a novel two-sided sequent calculus for types, supporting refined notions of well-typing and ill-typing, and explores internalising negation for improved semantics.
Findings
Supports more precise data-flow typing with constructors and pattern matching
Guarantees well-typed programs don't go wrong and ill-typed programs don't evaluate
Proposes an alternative semantics internalising meta-level negation
Abstract
We introduce two-sided type systems, which are 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 more refined notions of well-typing and ill-typing, guaranteeing both that well-typed programs don't go wrong and that ill-typed programs don't 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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Software Engineering Research · Formal Methods in Verification
