pith. sign in

arxiv: 2510.13725 · v3 · submitted 2025-10-15 · 💻 cs.PL

A Complementary Approach to Incorrectness Typing

Celia Mengyue Li , Sophie Pull , Steven Ramsay This is my paper

Pith reviewed 2026-05-18 06:34 UTC · model grok-4.3

classification 💻 cs.PL
keywords incorrectness typingcomplement operatornormal formstwo-sided type systemsrefutation principlespattern matchingfunctional programssubtyping decidability
0
0 comments X

The pith

Defining types over sets of normal forms allows a complement operator to act as negation in a two-sided type system for proving both correctness and incorrectness of programs.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces a type system that verifies both when functional programs with atoms and pattern matching are correct and when they are incorrect. By letting types denote sets of normal forms instead of values, the authors define a complement operator that functions as negation on typing formulas. This operator supports derivation of multiple refutation principles, including a type-theoretic version of co-implication, which are applied to show that certain programs go wrong. The system is proven sound and complete for normal forms, while the subtyping axiomatisation for the complement operator is shown to be decidable.

Core claim

By defining types to range over sets of normal forms rather than values, the authors introduce a complement operator on types that acts as negation on typing formulas. This operator enables derivation of a wide range of refutation principles inside a single two-sided type system, including the analogue of co-implication. The resulting system is sound and complete for normal forms, and an expressive axiomatisation of the complement via subtyping is decidable.

What carries the argument

The complement operator on types, which acts as negation on typing formulas when types range over sets of normal forms rather than values.

If this is right

  • Refutation principles such as the type-theoretic analogue of co-implication can be derived inside the type system.
  • Erlang-like programs can be certified to go wrong using the refutation principles.
  • The axiomatisation of the complement operator via subtyping is decidable.
  • The type system is sound and complete for normal forms.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This two-sided approach might integrate into existing type checkers to detect both safe and unsafe behaviors in one pass.
  • Completeness for normal forms could support exhaustive bug-finding tools for terminating functional programs.
  • The normal-form focus might extend naturally to languages with similar pattern-matching constructs beyond Erlang.

Load-bearing premise

Defining types to range over sets of normal forms rather than values is sufficient to define a complement operator that acts as a negation on typing formulas and enables derivation of refutation principles.

What would settle it

A concrete program with atoms and pattern matching that goes wrong yet admits no derivation of incorrectness using the complement operator, or a subtyping judgment involving the complement operator that the axiomatisation cannot decide.

Figures

Figures reproduced from arXiv: 2510.13725 by Celia Mengyue Li, Sophie Pull, Steven Ramsay.

Figure 1
Figure 1. Figure 1: Subtype relation on types semantics [[𝐴]]∗ for both argument and result since our calling convention is call-by-name (but see also Remark 1). Note that the type 𝐴 → 𝐵 is never empty, since it always contains 𝜆𝑥. div – a function that inevitably diverges certainly satisfies the condition on membership. The semantics of types justifies the following further abbreviations: Bot := Top𝑐 Pair := (Top, Top) PairV… view at source ↗
Figure 2
Figure 2. Figure 2: Two-Sided Type System. The Match Rule. In the (Match)rule, we abuse notation by considering a pattern-type substitution 𝜃, which is formally a finite map from term variables to types, also as a set of typings {𝑥 : 𝐴 | 𝜃(𝑥) = 𝐴}. The rule allows free choice of a pattern substitution 𝜃, so long as it satisfies the side condition PatSubst(𝑝, 𝜃). This requires that any type 𝜃(𝑥) chosen as the type of a free va… view at source ↗
Figure 3
Figure 3. Figure 3: Admissible rules for weakening, projections and conditionals. [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Derivable rules related to refutation. Similarly, by (MatchE) and (PairE), we can refute evaluation for e.g. scrutinizing a term that does not match any pattern, or trying to form a pair where one of the components does not evaluate. However, in each case, it is the term itself that directly goes wrong. What about if we want to show that, for example, a redex (𝜆𝑥. 𝑀) 𝑁 is contracted successfully, but that … view at source ↗
Figure 5
Figure 5. Figure 5: Derivable abstraction and application rules [PITH_FULL_IMAGE:figures/full_fig_p018_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Alternative rules for subtyping. 6 Metatheory of Subtyping The rules of the subtype relation are natural from our understanding of types as certain sets of normal forms, so it is not surprising that these sets form a model of the theory, as revealed by Theorem 6.1. The contrapositive of the theorem allows us to use the set-theoretic model to exclude that certain subtype inequalities are derivable. For exam… view at source ↗
Figure 7
Figure 7. Figure 7: One-sided typing rules (differences). subexpressions of the type 𝐵. Then consider the following set of types: A𝐴,𝐵 := SubExp(𝐴) ∪ SubExp(𝐵) ∪ {Top, Int, Pair, PairVal, Fun, Atom, Ok} This set consists of all the finitely many types that occur as subexpressions of the input types 𝐴 and 𝐵 as well as certain fixed types such as Top, Int and so on. Then define the following finite set of types: U𝐴,𝐵 := A𝐴,𝐵 ∪ … view at source ↗
Figure 8
Figure 8. Figure 8: One-sided Typing. Lemma C.1. The following rules are admissible in the system of [PITH_FULL_IMAGE:figures/full_fig_p037_8.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper introduces a two-sided type system for verifying the correctness and incorrectness of functional programs with atoms and pattern matching. A key idea is that types range over sets of normal forms rather than values, which enables definition of a complement operator on types that acts as negation on typing formulas. This allows derivation of a range of refutation principles, including a type-theoretic analogue of co-implication, which are used to certify that certain Erlang-like programs go wrong. An expressive axiomatisation of the complement operator via subtyping is shown decidable, and the overall type system is shown to be sound and complete for normal forms.

Significance. If the central claims hold, the work offers a distinctive approach to incorrectness reasoning within type systems by shifting the domain to normal forms and introducing a well-behaved complement operator. This unifies positive and negative verification in a single framework and supports derivation of refutation principles directly inside the type system. The decidability result for subtyping and the completeness property for normal forms are concrete strengths that could make the system practically relevant for static analysis of pattern-matching programs.

minor comments (2)
  1. The abstract would be strengthened by a single sentence clarifying the precise language fragment (e.g., the treatment of atoms and the form of pattern matching) before stating the main results.
  2. Consider adding a short illustrative derivation in an early section showing how the complement operator is applied to a concrete type to obtain a refutation judgment.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive and constructive review, and for recommending acceptance of the paper. We are glad that the referee found the shift to types over normal forms, the complement operator, the derived refutation principles, the decidability result, and the completeness property to be strengths of the work.

Circularity Check

0 steps flagged

No significant circularity; derivation self-contained via new definitions and standard proofs

full rationale

The paper defines types as ranging over sets of normal forms (rather than values) to introduce a complement operator that acts as negation on typing judgments. Soundness, completeness for normal forms, and decidability of the subtyping axiomatisation for the complement are established through direct proofs on the type system rules for functional programs with atoms and pattern matching. No load-bearing step reduces by construction to a fitted parameter, self-citation chain, or renamed known result; the refutation principles follow from the internal definition of complement and co-implication. The system is self-contained against external benchmarks for type soundness and decidability.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The approach relies on standard type theory background plus the novel definition of types over normal forms and the complement operator. No free parameters or invented entities beyond the complement are evident from the abstract.

axioms (1)
  • domain assumption Types range over sets of normal forms rather than values.
    This is the key modeling choice stated in the abstract that enables the complement operator.
invented entities (1)
  • Complement operator on types no independent evidence
    purpose: Acts as negation on typing formulas to derive refutation principles.
    Introduced as the central new construct; no independent evidence provided in abstract.

pith-pipeline@v0.9.0 · 5649 in / 1091 out tokens · 27535 ms · 2026-05-18T06:34:28.610032+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

36 extracted references · 36 canonical work pages

  1. [1]

    Wimmers, and T

    Alexander Aiken, Edward L. Wimmers, and T. K. Lakshman. 1994. Soft Typing with Conditional Types. InConference Record of POPL’94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, USA, January 17-21, 1994. 163–173. https://doi.org/10.1145/174675.177847

    work page doi:10.1145/174675.177847 1994

  2. [2]

    Pedro Carrott, Sacha-Élie Ayoun, and Azalea Raad. 2025. Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness. In39th European Conference on Object-Oriented Programming (ECOOP 2025) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 333), Jonathan Aldrich and Alexandra Silva (Eds.). Schloss Dagst...

    work page doi:10.4230/lipics.ecoop 2025

  3. [3]

    2024.Programming with Union, Intersection, and Negation Types

    Giuseppe Castagna. 2024.Programming with Union, Intersection, and Negation Types. Springer International Publishing, Cham, 309–378. https://doi.org/10.1007/978-3-031-34518-0_12

    work page doi:10.1007/978-3-031-34518-0_12 2024

  4. [4]

    Giuseppe Castagna, Mickaël Laurent, Kim Nguy˜ên, and Matthew Lutze. 2022. On Type-Cases, Union Elimination, and Occurrence Typing.Proc. ACM Program. Lang.6, POPL, Article 13 (Jan. 2022), 31 pages. https://doi.org/10.1145/3498674

    work page doi:10.1145/3498674 2022

  5. [5]

    Giuseppe Castagna and Zhiwu Xu. 2011. Set-theoretic foundation of parametric polymorphism and subtyping. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming(Tokyo, Japan)(ICFP ’11). Association for Computing Machinery, New York, NY, USA, 94–106. https://doi.org/10.1145/2034773.2034788

    work page doi:10.1145/2034773.2034788 2011

  6. [6]

    Vikraman Choudhury and Simon J. Gay. 2025. The Duality of 𝜆-Abstraction.Proc. ACM Program. Lang.9, POPL, Article 12 (Jan. 2025), 30 pages. https://doi.org/10.1145/3704848

    work page doi:10.1145/3704848 2025

  7. [8]

    Patrick Cousot, Radhia Cousot, and Francesco Logozzo. 2011. Precondition Inference from Intermittent Assertions and Application to Contracts on Collections. InVerification, Model Checking, and Abstract Interpretation, Ranjit Jhala and David Schmidt (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 150–168. https://doi.org/10.1007/978-3-642- 18275-4_12

    work page doi:10.1007/978-3-642- 2011

  8. [9]

    Tristan Crolard. 2001. Subtractive logic.Theoretical Computer Science254, 1 (2001), 151–185. https://doi.org/10.1016/ S0304-3975(99)00124-3

    work page 2001

  9. [10]

    Tristan Crolard. 2004. A Formulae-as-Types Interpretation of Subtractive Logic.J. Log. Comput.14, 4 (2004), 529–570. https://doi.org/10.1093/LOGCOM/14.4.529 28 Celia Mengyue Li, Sophie Pull, and Steven Ramsay

    work page doi:10.1093/logcom/14.4.529 2004

  10. [11]

    Jana Dunfield and Neel Krishnaswami. 2021. Bidirectional Typing.ACM Comput. Surv.54, 5, Article 98 (May 2021), 38 pages. https://doi.org/10.1145/3450952

    work page doi:10.1145/3450952 2021

  11. [12]

    Erlang/OTP 28. 2025. Dialyzer v5.4. Last accessed: 1/7/2025

    work page 2025

  12. [13]

    2013.Learn You Some Erlang for Great Good!No Starch Press

    Fred Hébert. 2013.Learn You Some Erlang for Great Good!No Starch Press. As of 6/6/2025, the examples can be viewed directly at https://learnyousomeerlang.com/dialyzer#type-inference-and-discrepancies

    work page 2013

  13. [14]

    Robert Jakob and Peter Thiemann. 2015. A Falsification View of Success Typing. InNASA Formal Methods, Klaus Havelund, Gerard Holzmann, and Rajeev Joshi (Eds.). Springer International Publishing, Cham, 234–247. https: //doi.org/10.1007/978-3-319-17524-9_17

    work page doi:10.1007/978-3-319-17524-9_17 2015

  14. [15]

    Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn. 2022. Finding Real Bugs in Big Programs with Incorrectness Logic.Proc. ACM Program. Lang.6, OOPSLA1, Article 81 (apr 2022), 27 pages. https://doi.org/10.1145/3527325

    work page doi:10.1145/3527325 2022

  15. [16]

    Tobias Lindahl and Konstantinos Sagonas. 2006. Practical Type Inference Based on Success Typings. InProceedings of the 8th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming(Venice, Italy)(PPDP ’06). Association for Computing Machinery, New York, NY, USA, 167–178. https://doi.org/10.1145/1140335.1140356

    work page doi:10.1145/1140335.1140356 2006

  16. [17]

    Julian Mackay, Susan Eisenbach, James Noble, and Sophia Drossopoulou. 2022. Necessity Specifications for Robustness. Proc. ACM Program. Lang.6, OOPSLA2, Article 154 (oct 2022), 30 pages. https://doi.org/10.1145/3563317

    work page doi:10.1145/3563317 2022

  17. [18]

    Robin Milner. 1978. A theory of type polymorphism in programming.J. Comput. System Sci.17, 3 (1978), 348–375. https://doi.org/10.1016/0022-0000(78)90014-4

    work page doi:10.1016/0022-0000(78)90014-4 1978

  18. [19]

    Tamás Nagy and Anikó Nagyné Víg. 2008. Erlang testing and tools survey. InProceedings of the 7th ACM SIGPLAN Workshop on ERLANG(Victoria, BC, Canada)(ERLANG ’08). Association for Computing Machinery, New York, NY, USA, 21–28. https://doi.org/10.1145/1411273.1411277

    work page doi:10.1145/1411273.1411277 2008

  19. [20]

    Peter W. O’Hearn. 2019. Incorrectness Logic.Proc. ACM Program. Lang.4, POPL, Article 10 (dec 2019), 32 pages. https://doi.org/10.1145/3371078

    work page doi:10.1145/3371078 2019

  20. [21]

    Lionel Parreaux and Chun Yin Chau. 2022. MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types.Proc. ACM Program. Lang.6, OOPSLA2, Article 141 (oct 2022), 30 pages. https://doi.org/10.1145/3563304

    work page doi:10.1145/3563304 2022

  21. [22]

    David J. Pearce. 2013. Sound and Complete Flow Typing with Unions, Intersections and Negations. InVerification, Model Checking, and Abstract Interpretation, Roberto Giacobazzi, Josh Berdine, and Isabella Mastroeni (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 335–354

    work page 2013

  22. [23]

    Luís Pinto and Tarmo Uustalu. 2009. Proof Search and Counter-Model Construction for Bi-intuitionistic Propositional Logic with Labelled Sequents. InAutomated Reasoning with Analytic Tableaux and Related Methods, Martin Giese and Arild Waaler (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 295–309

    work page 2009

  23. [24]

    Andrew M. Pitts. 2012. Lecture Notes on Types for Part II of the Computer Science Tripos. (2012). Page 2. Available from https://www.cl.cam.ac.uk/teaching/1213/Types/typ-notes.pdf, last accessed 18/07/2025

    work page 2012

  24. [25]

    Kelvin Qian, Scott Smith, Brandon Stride, Shiwei Weng, and Ke Wu. 2024. Semantic-Type-Guided Bug Finding.Proc. ACM Program. Lang.8, OOPSLA2, Article 348 (Oct. 2024), 28 pages. https://doi.org/10.1145/3689788

    work page doi:10.1145/3689788 2024

  25. [26]

    Azalea Raad, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn. 2022. Concurrent Incorrectness Separation Logic. Proc. ACM Program. Lang.6, POPL, Article 34 (jan 2022), 29 pages. https://doi.org/10.1145/3498695

    work page doi:10.1145/3498695 2022

  26. [27]

    Steven Ramsay and Charlie Walpole. 2024. Ill-Typed Programs Don’t Evaluate.Proc. ACM Program. Lang.8, POPL, Article 67 (Jan 2024), 31 pages. https://doi.org/10.1145/3632909

    work page doi:10.1145/3632909 2024

  27. [28]

    Cecylia Rauszer. 1974. A Formalization of the Propositional Calculus of H-B Logic.Studia Logica: An International Journal for Symbolic Logic33, 1 (1974), 23–34. http://www.jstor.org/stable/20014691

    work page arXiv 1974

  28. [29]

    Konstantinos Sagonas. 2021. Fifteen years of successfully dialyzing Erlang and Elixir code (invited talk). InProceedings of the 20th ACM SIGPLAN International Workshop on Erlang(Virtual, Republic of Korea)(Erlang 2021). Association for Computing Machinery, New York, NY, USA, 1. https://doi.org/10.1145/3471871.3480952

    work page doi:10.1145/3471871.3480952 2021

  29. [30]

    Luca Tranchini. 2017. Natural deduction for bi-intuitionistic logic.Journal of Applied Logic25 (2017), S72–S96. https://doi.org/10.1016/j.jal.2017.12.001 Logical Investigations on Assertion and Denial

    work page doi:10.1016/j.jal.2017.12.001 2017

  30. [31]

    A. S. Troelstra and H. Schwichtenberg. 2000.Basic Proof Theory(2 ed.). Cambridge University Press

    work page 2000

  31. [32]

    Hiroshi Unno, Yuki Satake, and Tachio Terauchi. 2017. Relatively Complete Refinement Type System for Verification of Higher-Order Non-Deterministic Programs.Proc. ACM Program. Lang.2, POPL, Article 12 (dec 2017), 29 pages. https://doi.org/10.1145/3158100

    work page doi:10.1145/3158100 2017

  32. [33]

    Robin Webbers, Klaus von Gleissenthall, and Ranjit Jhala. 2024. Refinement Type Refutations.Proc. ACM Program. Lang.8, OOPSLA2, Article 305 (Oct. 2024), 26 pages. https://doi.org/10.1145/3689745

    work page doi:10.1145/3689745 2024

  33. [34]

    Zhe Zhou, Ashish Mishra, Benjamin Delaware, and Suresh Jagannathan. 2023. Covering All the Bases: Type-Based Verification of Test Input Generators.Proc. ACM Program. Lang.7, PLDI, Article 157 (June 2023), 24 pages. https: //doi.org/10.1145/3591271

    work page doi:10.1145/3591271 2023

  34. [35]

    Noam Zilberstein, Derek Dreyer, and Alexandra Silva. 2023. Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning.Proc. ACM Program. Lang.7, OOPSLA1, Article 93 (apr 2023), 29 pages. https: A Complementary Approach to Incorrectness Typing 29 //doi.org/10.1145/3586045 30 Celia Mengyue Li, Sophie Pull, and Steven Ramsay A Supplemen...

    work page doi:10.1145/3586045 2023

  35. [36]

    Then by the induction hypothosis we have𝜃 1 ⊑𝜃 ′ 1 and𝜃 2 ⊑𝜃 ′

    work page

  36. [37]

    Sincedom(𝜃) =dom(𝜃 ′) =FV(𝑝 1)∪FV(𝑝 2),𝜃⊑𝜃 ′ follows directly. □ Definition D.5 (Coherence of Term and Pattern Type Substitutions under Contexts).Let 𝜎 be a term substitution (mapping term variables to terms), 𝜃 a pattern type substitution (mapping term variables to types), andΓ,∆left and right contexts respectively. We define thecoherence relation Γ⊢𝜎::𝜃...

    work page