Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Complementary Approach to Incorrectness Typing

Celia Mengyue Li, Sophie Pull, Steven Ramsay

TL;DR

This paper introduces a novel two-sided type system that reasons about both correctness and incorrectness by interpreting types as sets of normal forms and by introducing a complement operator. The central innovations include the complement on normal forms, the coarrow (A ³ B) type, and a small, coherent set of rules (notably Match and CompR) that derive powerful refutation principles alongside traditional typing. It demonstrates practical applicability by certifying Erlang-style Hébert examples go wrong, and establishes soundness, a decidable subtyping relation, and completeness for normal forms, while connecting to bi-intuitionistic logic through the coarrow construct. The work positions itself as a unified foundation for reasoning about incorrectness in functional languages and lays groundwork for further developments in type-based verification of faulty behavior. Overall, it advances the theory and practice of incorrectness typing with a principled, decidable framework and meaningful connections to existing logics and type systems.

Abstract

We introduce a new two-sided type system for verifying the correctness and incorrectness of functional programs with atoms and pattern matching. A key idea in the work is that types should range over sets of normal forms, rather than sets of values, and this allows us to define a complement operator on types that acts as a negation on typing formulas. We show that the complement allows us to derive a wide range of refutation principles within the system, including the type-theoretic analogue of co-implication, and we use them to certify that a number of Erlang-like programs go wrong. An expressive axiomatisation of the complement operator via subtyping is shown decidable, and the type system as a whole is shown to be not only sound, but also complete for normal forms.

A Complementary Approach to Incorrectness Typing

TL;DR

This paper introduces a novel two-sided type system that reasons about both correctness and incorrectness by interpreting types as sets of normal forms and by introducing a complement operator. The central innovations include the complement on normal forms, the coarrow (A ³ B) type, and a small, coherent set of rules (notably Match and CompR) that derive powerful refutation principles alongside traditional typing. It demonstrates practical applicability by certifying Erlang-style Hébert examples go wrong, and establishes soundness, a decidable subtyping relation, and completeness for normal forms, while connecting to bi-intuitionistic logic through the coarrow construct. The work positions itself as a unified foundation for reasoning about incorrectness in functional languages and lays groundwork for further developments in type-based verification of faulty behavior. Overall, it advances the theory and practice of incorrectness typing with a principled, decidable framework and meaningful connections to existing logics and type systems.

Abstract

We introduce a new two-sided type system for verifying the correctness and incorrectness of functional programs with atoms and pattern matching. A key idea in the work is that types should range over sets of normal forms, rather than sets of values, and this allows us to define a complement operator on types that acts as a negation on typing formulas. We show that the complement allows us to derive a wide range of refutation principles within the system, including the type-theoretic analogue of co-implication, and we use them to certify that a number of Erlang-like programs go wrong. An expressive axiomatisation of the complement operator via subtyping is shown decidable, and the type system as a whole is shown to be not only sound, but also complete for normal forms.
Paper Structure (35 sections, 36 theorems, 31 equations, 8 figures)

This paper contains 35 sections, 36 theorems, 31 equations, 8 figures.

Table of Contents

  1. Introduction
  2. A Two-Sided System with Complement on Normal Forms
  3. Contributions
  4. Outline
  5. A Functional Programming Language
  6. Abbreviations
  7. Two-Sided System
  8. Subtype Relation
  9. Typing Relation
  10. The Match Rule
  11. The CompR Rule
  12. Refutation
  13. Hébert's Examples
  14. The CoArrow Type
  15. Metatheory of Subtyping
  16. ...and 20 more sections

Key Result

lemma 1

The stuck terms may equivalently be described by the following grammar:

Figures (8)

  • Figure 1: Subtype relation on types
  • Figure 2: Two-Sided Type System.
  • Figure 3: Admissible rules for weakening, projections and conditionals.
  • Figure 4: Derivable rules related to refutation.
  • Figure 5: Derivable abstraction and application rules ala bi-intuitionistic logic.
  • ...and 3 more figures

Theorems & Definitions (53)

  • definition 1: Terms and Patterns
  • definition 2: Reduction
  • definition 3: Normal forms, values, stuck terms and going wrong
  • lemma 1: Stuck Terms
  • definition 4: Types
  • Remark 1
  • definition 5: Subtyping Relations
  • definition 6: Typing Formula
  • definition 7: Typing Judgement and Derivability
  • Remark 2
  • ...and 43 more