Pith. sign in

REVIEW 3 major objections 4 minor 49 references

Orthologic Type Systems

T0 review · 3 major / 4 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper proves that subtyping with union, intersection, and negation types under assumptions is decidable in quadratic time and that every type has a quadratic-time normal form that is the smallest equivalent type.

desk verdict Solid formally verified subtyping algorithm for ortholattices with constructors; the normalization half is a sketched proof that needs a careful referee before the minimal-form claim is trusted. read the letter →

arxiv 2507.10482 v1 pith:JBNBPTGV submitted 2025-07-14 cs.PL cs.LO

Simon Guilloud , Viktor Kunčak This is my paper · ORCID
classification cs.PLcs.LO
keywords orthologicortholatticessubtypinguniontypesintersectionnegationtypeconstructorsnormalization
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper proposes using orthologic, the logic of ortholattices, as a foundation for type systems with intersection, union, and negation types, where negation behaves like a complement but distributivity is not assumed. Its central claim is that adding (anti)monotone type constructors and user-supplied subtyping assumptions preserves the efficient behavior of pure orthologic: subtyping entailment is decidable in $O(n^2(1+m))$ time, where $m$ is the number of assumptions, and every type can be normalized in quadratic time to the unique smallest equivalent type. If this holds, type checkers could gain complete and predictable reasoning about union and intersection types without the exponential blow-ups caused by distributivity in current languages.

What carries the argument

The load-bearing mechanism is partial cut elimination for the sequent calculus SC+ (Theorem 4.7), which removes all uses of transitivity except those involving axioms and gives a subformula property: any derivable inequality $S \leq T$ has a proof built only from subterms of $S$, $T$, and the axioms. This turns proof search into a finite closure problem expressed as a set of Horn clauses with at most three literals each, solvable in linear time. The second mechanism is the syntactic characterization of minimal terms in BL+ (Theorem 6.6), which says a disjunction of normal terms is minimal exactly when its disjuncts form an antichain and no conjunct inside a disjunct is below the whole disjunction; the transformations $\zeta$, $\eta$, $\delta$, and $\beta$ enforce these conditions while preserving equivalence, and their composition yields the OL+ normal form.

What would settle it

Enumerate small terms in the range of the $\beta$ reduction and check whether $\vdash_{CF+_\delta} S_L,S_L$ holds exactly when $S\sim_{BL+}0$; a mismatch for any single term would refute Lemma 6.13 and hence Theorem 6.15.

Watch

Extended reading notes

Core claim

The paper establishes that the entailment problem for OL+, the class of ortholattices with monotonic, antimonotonic, and invariant function symbols, is decidable in polynomial time even in the presence of axioms. It gives a sequent calculus SC+ that is sound and complete for OL+ with axioms, proves partial cut elimination (Theorem 4.7) so that every provable sequent has a proof using only subterms of the goal and the axioms, and then reduces proof search to a polynomial-size set of propositional Horn clauses, yielding the $O(n^2(1+|A|))$ decision procedure of Theorem 4.1. For normalization, it characterizes the minimal forms of BL+, bounded lattices with monotone functions, by Whitman-style conditions (Theorem 6.6), constructs a quadratic-time normal form function for BL+, and lifts it to OL+ by pushing negations onto literals and function symbols, obtaining a quadratic-time function that maps each term to the unique smallest term in its equivalence class (Theorem 6.15).

Load-bearing premise

The normalization theorem rests on the unformalized step in Lemma 6.13: if a term $S$ in the negation-normal fragment admits the derivation $S_L,S_L$, then $S$ is equivalent to bottom already in BL+; if that inference fails, the quadratic minimal-normal-form result for OL+ collapses.

Editorial extensions

If this is right

  • Subtyping in a language with intersection, union, and negation types, covariant and contravariant type constructors, and subtyping constraints can be decided in $O(n^2(1+m))$ time instead of exponential time.
  • Type simplifiers can use the normalization function to replace every type by the unique smallest equivalent type in quadratic time, never increasing the size of the representation.
  • Because the semantics is the free ortholattice with monotone functions, any subtyping judgment the algorithm accepts remains valid if new types or constructors are added later, an open-world property.
  • Record types, nominal subtyping declarations, and constrained polymorphism can be encoded as axioms, so the decision procedure applies to these features directly.
  • The system deliberately omits distributivity and constructor conjunctivity, matching languages whose type lattices are non-distributive and avoiding unsound laws found in some compilers.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The Horn-clause encoding suggests that subtyping queries under a fixed axiom set can be solved incrementally, with new clauses added as constraints are learned, which may yield further speedups in compilers.
  • The minimal normal form could serve as a canonical key for hash-consing types, making equivalence tests constant-time within a compilation session.
  • The partial cut elimination result may transfer to other substructural or non-classical logics with monotone operators, where similar Horn-clause encodings would give polynomial decision procedures.
  • An empirical test on the benchmark families described in the paper (for example the alternating union-intersection types that make current compilers slow) would show whether the predicted quadratic behavior replaces the observed exponential growth.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper proposes orthologic with monotone and antimonotone function symbols (OL+) as a foundation for subtyping with intersection, union, and negation types plus type constructors. It presents a sequent calculus SC+ for OL+ with axioms, proves soundness and completeness, and states a partial cut-elimination theorem (Theorem 4.7) that is formalized in Rocq. From cut elimination it derives an O(n^2(1+|A|)) decision procedure for the entailment problem by reducing proof search to propositional Horn clauses (Theorems 4.1 and 5.1). It then develops a normal-form theory for bounded lattices with monotone functions (BL+), gives a quadratic-time normalization algorithm for BL+ (Theorem 6.8), and extends it to OL+ through the maps delta, beta, zeta, and eta (Theorems 6.12, 6.13, and 6.15), claiming a unique minimal-size canonical form. The paper explicitly states that not all results in Section 6 are formalized in Rocq.

Significance. If the results hold, this is a valuable contribution: it offers a rare combination of expressiveness (negation, union/intersection, variance, and subtyping assumptions) with polynomial-time subtyping and normalization, and it ships a Rocq formalization of the central cut-elimination and completeness theorems, together with a clean reduction of proof search to Horn clauses. The paper is also careful about scope, explicitly acknowledging limitations such as the lack of support for recursive type definitions with parameters. The main weakness is that the normalization half of the paper rests on Lemma 6.12, whose proof contains an unsubstantiated step, and the paper notes that Section 6 was not fully formalized. Until that step is proved, the minimal-canonical-form claim should be treated as conditional, so the paper requires revision before the normalization contribution can be accepted.

major comments (3)
  1. [Section 6.1, Lemma 6.12] The proof of the disjunctive case states, "If S = phi1 \/ phi2 ~OL+ 1 then S = 1 by definition of beta," but gives no derivation. For this step to be valid, phi1 \/ phi2 ~OL+ 1 must imply that at least one of the two bounded-lattice inequalities checked by Algorithm 4 holds, namely delta(neg phi1) <=BL+ phi1 \/ phi2 or delta(neg phi2) <=BL+ phi1 \/ phi2. This implication is not a formal consequence of the ortholattice laws: in an ortholattice, phi1 \/ phi2 = 1 is equivalent to neg phi1 /\ neg phi2 = 0, and the latter does not by itself yield a bounded-lattice inequality in the free BL+, which has no complementation structure. The paper gives no argument that beta-normalized terms exclude possible failure cases. Because Lemma 6.12 is used in the Replace case of Lemma 6.13, this gap is load-bearing for the whole normalization development.
  2. [Section 6, Lemma 6.13 and Theorem 6.15] The Replace case of Lemma 6.13 contains the inference "if |- CF+_delta S_L, S_L holds, then S ~OL+ 0; hence, by Lemma 6.12, S ~BL+ 0." This is the only bridge between OL+ equivalence and BL+ equivalence in the normalization construction, and it is used in Theorem 6.15 to conclude that beta(delta(S)) ~BL+ beta(delta(T)) whenever S ~OL+ T. That conclusion is exactly what makes eta(zeta(beta(delta(S)))) well-defined on OL+ equivalence classes. The paper notes that not all results in Section 6 were formalized in Rocq, so there is no machine-checked fallback for this step. If Lemma 6.12 cannot be repaired, Theorem 6.15 and the minimal-canonical-form claim collapse; as written, the proof is incomplete.
  3. [Section 6, Theorem 6.6] In the proof of Theorem 6.6, in the join case with S = x, the text says "x <=BL+ T1 \/ ... \/ Tn and hence necessarily forall i, x <=BL+ Ti." This is incorrect as stated for free lattices: a generator below a join is below at least one joinand, not necessarily below all of them. The subsequent contradiction relies on the interaction between this step and the dual inequality T1 \/ ... \/ Tn <=BL+ x. If "forall" is a typo for "exists," the argument needs to be restated carefully; if not, the proof of this case is invalid. Since Theorem 6.6 is the basis for the BL+ normal-form characterization and hence for Theorem 6.8, this needs correction.
minor comments (4)
  1. [Abstract and Theorem 4.1] The abstract states the complexity as O(n^2(1+m)) while Theorem 4.1 states O(n^2(1+|A|)); the relationship between m and |A| (number of axioms vs. total size of axioms) should be clarified, and the missing closing parenthesis in Theorem 4.1 should be fixed.
  2. [Algorithm 1] The pseudocode uses a special value "None" in sequents, but the formal system of Section 4 has only two annotated terms and no None constructor; lines 20 and 24 should be explained or the pseudocode should be aligned with the formal system. Lines 32-33 say "analogous" and should be spelled out.
  3. [Section 6, Definition 6.9] The sentence "Define OL+ (resp BL+) as the algebraic signature of OL+ (resp BL+) extended with ..." is grammatically unclear and should be rephrased.
  4. [References] References [24] and [25] appear to be the same work (Henglein and Rehof, Constraint Automata and the Complexity of Recursive Subtype Entailment) and should be merged or distinguished.

Circularity Check

1 steps flagged · score 6.0 of 10

OL+ minimal-normal-form theorem relies on Lemma 6.12, whose disjunctive case is asserted 'by definition of β' instead of proved.

  1. self definitional [Section 6.1, Lemma 6.12, proof of the disjunctive case]
    "If S=φ1∨φ2∼OL+1 then S=1 by definition of β."

    Lemma 6.12 asserts that on β-normalized terms, OL+-equivalence to 1 coincides with BL+-equivalence to 1. The disjunctive case is dismissed with 'then S=1 by definition of β.' Algorithm 4 defines β to return 1 only when a specific BL+-inequality holds; it does not define OL+-validity of a disjunction. Inferring S=1 from S∼OL+1 requires already knowing that every β-normalized disjunction equivalent to 1 in OL+ triggers β's collapse, which is precisely the lemma's completeness direction. Thus the target equivalence is assumed inside the definition of β, not proved.

full rationale

The subtyping side of the paper is self-contained: Theorems 4.4, 4.5 and 4.7 construct the quotient algebra and the Horn-clause reduction, and the key cut-elimination theorem is formalized in Rocq, so the O(n^2(1+m)) entailment algorithm does not reduce to a fitted parameter or to an unverified self-citation. The citations to the authors' earlier orthologic results [21,22] are legitimate external support: [21] is peer-reviewed and [22] is a machine-checked implementation. The circularity is confined to Section 6.1. Lemma 6.12's proof of the case S=φ1∨φ2∼OL+1 is the single sentence 'then S=1 by definition of β,' which turns the completeness of β's collapse condition into a definitional fact. That is a self-definitional reduction: the target property (β-normalized OL+ top-equivalence is captured by a BL+-checkable inequality) is read off from Algorithm 4 rather than established. Lemma 6.13 and Corollary 6.14 inherit this step, and Theorem 6.15's normalization function η(ζ(β(δ(S)))) depends on it; hence the claimed quadratic-time minimal canonical form for OL+ is only as strong as this unproved definitional identification. The paper explicitly warns that not all results in Section 6 were formalized in Rocq. Overall, the main subtyping contribution remains independent, so the circularity is partial rather than total.

Assumptions & free parameters 0 free parameters · 7 assumptions · 0 invented entities

The main new content rests on the ortholattice axioms, the monotonicity axiom for constructors, and finite axiom sets for subtyping assumptions. No free parameters are fitted to data. The paper's normality claims rely on two unformalized characterization lemmas, which are the main intellectual debt beyond the formalized cut elimination.

assumptions (7)
  • domain assumption Types form an ortholattice satisfying V1-V9 and V1'-V9'
    This is the design decision, stated in Section 1 and Definitions 3.2 and 3.4, that models types as an ortholattice rather than a distributive or Boolean lattice.
  • domain assumption Type constructors satisfy the monotonicity axiom V10 (or equivalently V10')
    Definition 3.3 and Theorem 5.2; this is the only law assumed about constructors, deliberately avoiding constructor conjunctivity laws like Equation (1).
  • domain assumption Subtyping contexts are finite sets of axioms A, and entailment is with respect to all OL+ algebras satisfying A
    Defined in Section 4 (fix the set of axioms A) and used in Theorem 4.1 and the Horn clause reduction.
  • standard math The quotient construction TOL+(X)/|-| is an ortholattice, and free algebra results justify soundness and completeness
    Theorem 4.5 uses standard universal algebra facts; Theorem 5.2 uses quasivariety and variety equivalence; these are standard background.
  • standard math Horn satisfiability is decidable in linear time by unit propagation (Dowling and Gallier)
    Invoked in Theorem 5.1; standard result.
  • ad hoc to paper Whitman-style conditions characterize minimal normal forms in free bounded lattices with monotone functions (Theorem 6.6)
    This characterization is stated and proved in the paper but is not machine-checked; it is load-bearing for the quadratic normalization claim, and the proof is a sketch.
  • ad hoc to paper Lemma 6.13 bridge between OL+ and BL+ sequent calculi
    States that CF+ can be replaced by CF+_BL after pseudo-negation normal form; the proof contains a terse step about S ~OL+ 0 and is not formalized.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Orthologic Type Systems." pith.science (2026). https://pith.science/paper/JBNBPTGV

@misc{pith2026250710482,
  author       = {Pith},
  title        = {Pith review of: Orthologic Type Systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/JBNBPTGV}},
  note         = {Machine review of arXiv:2507.10482}
}
abstract

We propose to use orthologic as the basis for designing type systems supporting intersection, union, and negation types in the presence of subtyping assumptions. We show how to extend orthologic to support monotonic and antimonotonic functions, supporting the use of type constructors in such type systems. We present a proof system for orthologic with function symbols, showing that it admits partial cut elimination. Using these insights, we present an $\mathcal O(n^2(1+m))$ algorithm for deciding the subtyping relation under $m$ assumptions. We also show $O(n^2)$ polynomial-time normalization algorithm, allowing simplification of types to their minimal canonical form.

Figures

Figures reproduced from arXiv: 2507.10482 by the authors.

Figure 1
Figure 1. Examples of Functions on Lattices with Monotonicity Properties [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Deduction rules of Orthologic. Each holds for arbitrary [PITH_FULL_IMAGE:figures/full_fig_p012_2.png] view at source ↗
Figure 3
Figure 3. Deduction rules of CF+ 𝐵𝐿. Theorem 6.4 (Soundness and Completeness of CF+ 𝐵𝐿, Rocq: CFBLPlus_soundness, CFBLPlus_completeness). For 𝑆,𝑇 ∈ TBL+ (𝑋), 𝑆 ≤BL+ 𝑃 if and only if 𝑆 ⊢CF+ 𝑃 is provable. Proof. As in Lemma 5.3; see also the formal proof in Rocq. □ We now state a useful inversion lemma for terms starting with a function symbol. Lemma 6.5. Let 𝑇 ∈ TBL+ (𝑋) be in minimal form and suppose 𝑇 ∼BL+ 𝐹 (𝑆𝑥1 , ..., 𝑆𝑦1… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

49 extracted references · 24 canonical work pages

  1. [1]

    Wimmers, and T

    Alexander Aiken, Edward L. Wimmers, and T. K. Lakshman. 1994. Soft Typing with Conditional Types. In Conference Record of POPL’94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, USA, January 17-21, 1994 , Hans-Juergen Boehm, Bernard Lang, and Daniel M. Yellin (Eds.). ACM Press, 163–173. doi:10.1145/174675.177847

    work page arXiv 1994

  2. [2]

    Olivier Blanvillain, Jonathan Immanuel Brachthäuser, Maxime Kjaer, and Martin Odersky. 2022. Type-level programming with match types. Proc. ACM Program. Lang. 6, POPL (2022), 1–24. doi:10.1145/3498698

    doi:10.1145/3498698 2022

  3. [3]

    Günter Bruns. 1976. Free Ortholattices. Canadian Journal of Mathematics 28, 5 (Oct. 1976), 977–985. doi:10.4153/CJM-1976-095-6

    doi:10.4153/cjm-1976-095-6 1976

  4. [4]

    Sankappanavar

    Stanley Burris and Hanamantagouda P. Sankappanavar. 1981. A course in universal algebra . Graduate texts in mathematics, Vol. 78. Springer

    work page 1981

  5. [5]

    Giuseppe Castagna. 2024. Programming with Union, Intersection, and Negation Types. In The French School of Programming, Bertrand Meyer (Ed.). Springer International Publishing, Cham, 309–378. doi:10.1007/978-3-031-34518-0_12

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

  6. [6]

    Mario Coppo and Mariangiola Dezani-Ciancaglini. 1980. An extension of the basic functionality theory for the 𝜆-calculus. Notre Dame J. Formal Log. 21, 4 (1980), 685–693. doi:10.1305/NDJFL/1093883253

    arXiv 1980

  7. [7]

    Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977 , Robert M. Graham, Michael A. Harrison, and Ravi Sethi (...

    arXiv 1977

  8. [8]

    Patrick Cousot and Radhia Cousot. 1979. Systematic Design of Program Analysis Frameworks. In Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, USA, January 1979 , Alfred V. Aho, Stephen N. Zilles, and Barry K. Rosen (Eds.). ACM Press, 269–282. doi:10.1145/567752.567778

    arXiv 1979

Show all 49 references
  1. [9]

    Mark Day, Robert Gruber, Barbara Liskov, and Andrew C. Myers. 1995. Subtypes vs. Where Clauses: Constraining Parametric Polymorphism. SIGPLAN Not. 30, 10 (Oct. 1995), 156–168. doi:10.1145/217839.217852

    1995

  2. [10]

    Informatica Universita di Torino

    Dip. Informatica Universita di Torino. 2014. TLCA List of Open Problems. https://tlca.di.unito.it/opltlca/

    2014

  3. [11]

    Stephen Dolan. 2017. Algebraic Subtyping: Distinguished Dissertation 2017 . BCS Learning & Development Ltd, Swindon, GBR

    2017

  4. [12]

    Dowling and Jean H

    William F. Dowling and Jean H. Gallier. 1984. Linear-Time Algorithms for Testing the Satisfiability of Propositional Horn Formulae. The Journal of Logic Programming 1, 3 (Oct. 1984), 267–284. doi:10.1016/0743-1066(84)90014-1

    1984 doi

  5. [13]

    Jana Dunfield and Frank Pfenning. 2004. Tridirectional typechecking. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004 , Neil D. Jones and Xavier Leroy (Eds.). ACM, 281–292. doi:10.1145...

    2004

  6. [14]

    Ralph Freese, Jaroslav Jezek, and J. Nation. 1995. Free Lattices. Mathematical Surveys and Monographs, Vol. 42. American Mathematical Society, Providence, Rhode Island. doi:10.1090/surv/042

    1995 doi

  7. [15]

    Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, and Robbert Krebbers

    Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, and Robbert Krebbers. 2020. Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris. Proc. ACM Program. Lang. 4, ICFP (2020), 114:1–114:29. doi:10.1145/3408996

    2020 doi

  8. [16]

    Simon Guilloud, Mario Bucev, Dragana Milovancevic, and Viktor Kuncak. 2023. Formula Normalizations in Verification. In 35th International Conference on Computer Aided Verification (Lecture Notes in Computer Science) . Springer, Paris, 398–422

    2023

  9. [17]

    Simon Guilloud, Sankalp Gambhir, Andrea Gilot, and Viktor Kuncak. 2024. Mechanized HOL Reasoning in Set Theory. In 15th International Conference on Interactive Theorem Proving (ITP 2024)

    2024

  10. [18]

    Simon Guilloud, Sankalp Gambhir, and Viktor Kuncak. 2023. LISA – A Modern Proof System. In 14th Conference on Interactive Theorem Proving (Leibniz International Proceedings in Informatics) . Daghstuhl, Bialystok, 17:1–17:19

    2023

  11. [19]

    Simon Guilloud, Sankalp Gambhir, and Viktor Kunčak. 2024. Interpolation and Quantifiers in Ortholattices. In Verification, Model Checking, and Abstract Interpretation: 25th International Conference, VMCAI 2024, London, United Kingdom, January 15–16, 2024, Proceedings, Part I ....

    2024 doi

  12. [20]

    Simon Guilloud and Viktor Kunčak. 2022. Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time. In Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science) , Dana Fisman and Grigore Rosu (Eds.). Springer Intern...

    2022 doi

  13. [21]

    Simon Guilloud and Viktor Kunčak. 2024. Orthologic with Axioms. Proceedings of the ACM on Programming Languages 8, POPL (Jan. 2024), 39:1150–39:1178. doi:10.1145/3632881

    2024 doi

  14. [22]

    Simon Guilloud and Clément Pit-Claudel. 2025. Verified and Optimized Implementation of Orthologic Proof Search. In Computer Aided Verification. Springer, Zagreb, 18. Orthologic Type Systems 27

    2025

  15. [23]

    Jad Hamza, Nicolas Voirol, and Viktor Kuncak. 2019. System FR: formalized foundations for the stainless verifier. Proc. ACM Program. Lang. 3, OOPSLA (2019), 166:1–166:30. doi:10.1145/3360592

    2019 doi

  16. [24]

    Fritz Henglein and Jakob Rehof. 1998. Constraint Automata and the Complexity of Recursive Subtype Entailment. In Automata, Languages and Programming, 25th International Colloquium, ICALP’98, Aalborg, Denmark, July 13-17, 1998, Proceedings (Lecture Notes in Computer Science, Vo...

    1998 doi

  17. [25]

    Fritz Henglein and Jakob Rehof. 1998. Constraint Automata and the Complexity of Recursive Subtype Entailment. In Proceedings of the 25th International Colloquium on Automata, Languages and Programming (ICALP ’98) . Springer-Verlag, Berlin, Heidelberg, 616–627

    1998

  18. [26]

    Shengyi Jiang, Chen Cui, and Bruno C. d. S. Oliveira. 2025. Bidirectional Higher-Rank Polymorphism with Intersection and Union Types. Bidirectional Higher-Rank Polymorphism with Intersection and Union Types (Artifact) 9, POPL (Jan. 2025), 71:2118–71:2148. doi:10.1145/3704907

    2025 doi

  19. [27]

    Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018), e20. doi:10.1017/S0956796818000151

    2018 doi

  20. [28]

    Tomoaki Kawano. 2018. Labeled Sequent Calculus for Orthologic. Bulletin of the Section of Logic 47, 4 (Dec. 2018), 217–232. doi:10.18778/0138-0680.47.4.01

    2018 doi

  21. [29]

    Filip Křikava, Heather Miller, and Jan Vitek. 2019. Scala Implicits Are Everywhere: A Large-Scale Study of the Use of Scala Implicits in the Wild. Artifact for Scala Implicits are Everywhere 3, OOPSLA (Oct. 2019), 163:1–163:28. doi:10.1145/3360589

    2019 doi

  22. [30]

    Kuncak and M

    V. Kuncak and M. Rinard. 2003. Structural Subtyping of Non-Recursive Types Is Decidable. 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings. 18 (2003), 96–107. doi:10.1109/LICS.2003.1210049

    2003 arXiv

  23. [31]

    Olivier Laurent. 2016. Focusing in Orthologic. In 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal (LIPIcs, Vol. 52) , Delia Kesner and Brigitte Pientka (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für ...

    2016 doi

  24. [32]

    Lionel Parreaux. 2025. Hkust-Taco/Mlscript. HKUST TACO Lab

    2025

  25. [33]

    MacQueen, Gordon D

    David B. MacQueen, Gordon D. Plotkin, and Ravi Sethi. 1986. An Ideal Model for Recursive Polymorphic Types. Inf. Control. 71, 1/2 (1986), 95–130. doi:10.1016/S0019-9958(86)80019-5

    1986 doi

  26. [34]

    Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. 1999. Principles of program analysis . Springer. doi:10.1007/978-3-662-03811-6

    1999 doi

  27. [35]

    Martin Odersky, Martin Sulzmann, and Martin Wehr. 1999. Type Inference with Constrained Types. Theory Pract. Object Syst. 5, 1 (1999), 35–55

    1999

  28. [36]

    Lionel Parreaux and Chun Yin Chau. 2022. MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types. Proceedings of the ACM on Programming Languages 6, OOPSLA2 (Oct. 2022), 141:449–141:478. doi:10.1145/3563304

    2022 doi

  29. [37]

    Meta Platforms. 2025. Documention: Guides and references for all you need to know about Flow. https://flow.org/en/docs/

    2025

  30. [38]

    François Pottier. 1996. Simplifying Subtyping Constraints. In Proceedings of the First ACM SIGPLAN International Conference on Functional Programming (ICFP ’96) . Association for Computing Machinery, New York, NY, USA, 122–133. doi:10.1145/232627.232642

    1996

  31. [39]

    François Pottier. 2001. Simplifying Subtyping Constraints: A Theory. Inf. Comput. 170, 2 (2001), 153–183. doi:10.1006/INCO.2001.2963

    2001

  32. [40]

    Bierman, and Panagiotis Vekris

    Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin M. Bierman, and Panagiotis Vekris. 2015. Safe & Efficient Gradual Typing for TypeScript. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January ...

    2015

  33. [41]

    Didier Rémy and François Pottier. 2004. Advanced Topics in Types and Programming Languages, Chapter 10 . The MIT Press, United States of America

    2004

  34. [42]

    Viorica Sofronie-Stokkermans. 2014. Hierarchical Reasoning in Local Theory Extensions and Applications. In 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2014, Timisoara, Romania, September 22-25, 2014 , Franz Winkler, Viorel N...

    2014 doi

  35. [43]

    Zhendong Su, Alexander Aiken, Joachim Niehren, Tim Priesnitz, and Ralf Treinen. 2002. The First-Order Theory of Subtyping Constraints. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’02). Association for Computing Machinery...

    2002

  36. [44]

    The CDuce Team. 2021. The CDuce Compiler. . https://www.cduce.org/ 28 Simon Guilloud and Viktor Kunčak

    2021

  37. [45]

    Jerzy Tiuryn. 1992. Subtype Inequalities. In Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS ’92), Santa Cruz, California, USA, June 22-25, 1992 . IEEE Computer Society, 308–315. doi:10.1109/LICS.1992.185543

    1992

  38. [46]

    Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, and Martin Sulzmann. 2011. OutsideIn(X) Modular Type Inference with Local Assumptions. Journal of Functional Programming 21, 4-5 (Sept. 2011), 333–412. doi:10.1017/S0956796811000098

    2011 doi

  39. [47]

    PHP Watch. 2020. Intersection Types in PHP 8.1. https://php.watch/versions/8.1/intersection-types Accessed: 2025-01-19

    2020

  40. [48]

    Philip M. Whitman. 1941. Free Lattices. Annals of Mathematics 42, 1 (1941), 325–330. doi:10.2307/1969001 jstor:1969001

    1941 doi

  41. [49]

    2015-2025

    ZpdDG4gta. 2015-2025. Negated types, #4196. https://github.com/microsoft/TypeScript/issues/4196 Orthologic Type Systems 29 A Additional Lemmas And Proofs Lemma A.1 (Substitution). Let𝐹(𝐴1,...,𝐴 𝑛) be a function symbol of arity 𝑛, and let𝐺 be an arbitrary term such that for eve...

    2015

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.