Ill-Typed Programs Don't Evaluate

Research output: Contribution to journalArticle (Academic Journal)peer-review

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 guarantees that ill-typed programs don't evaluate, but in which well-typed programs may yet go wrong.
Original languageEnglish
Article number67
Pages (from-to)2010–2040
Number of pages31
JournalProceedings of the ACM on Programming Languages
Volume8
Issue numberPOPL
DOIs
Publication statusPublished - 5 Jan 2024

Bibliographical note

Funding Information:
The first author is very grateful for an award from Meta Research.

Publisher Copyright:
© 2024 Copyright held by the owner/author(s).

Structured keywords

  • Programming Languages

Keywords

  • type systems
  • higher-order program verification
  • incorrectness

Fingerprint

Dive into the research topics of 'Ill-Typed Programs Don't Evaluate'. Together they form a unique fingerprint.

Cite this