Hubbry Logo
Refinement typeRefinement typeMain
Open search
Refinement type
Community hub
Refinement type
logo
7 pages, 0 posts
0 subscribers
Be the first to start a discussion here.
Be the first to start a discussion here.
Contribute something
Refinement type
Refinement type
Refinement type
View on Wikipedia
from Wikipedia
Type systems
General concepts
Major categories
Minor categories

In type theory, a refinement type[1][2][3] is a type endowed with a predicate which is assumed to hold for any element of the refined type. Refinement types can express preconditions when used as function arguments or postconditions when used as return types: for instance, the type of a function which accepts natural numbers and returns natural numbers greater than 5 may be written as . Refinement types are thus related to behavioral subtyping.

History

[edit]

The concept of refinement types was first introduced in Freeman and Pfenning's 1991 Refinement types for ML,[1] which presents a type system for a subset of Standard ML. The type system "preserves the decidability of ML's type inference" whilst still "allowing more errors to be detected at compile-time". In more recent times, refinement type systems have been developed (primary in academia) for languages such as Haskell[4][5], TypeScript[6], Rust[7], and as libraries for real world usage in Scala[8][9].

See also

[edit]

References

[edit]
Revisions and contributorsEdit on WikipediaRead on Wikipedia

Refinement type

View on Grokipedia
from Grokipedia
In and programming languages, a refinement type augments a base type—such as an or —with a logical predicate that precisely constrains the set of values it inhabits, allowing programmers to specify and enforce properties like non-negativity or bounds at . This approach combines the simplicity of standard s with the expressiveness of dependent types, but approximates the latter's full power using decidable , typically via SMT solvers, to ensure scalability and usability. Originating from early work on refining ML's to handle recursive subtypes of datatypes, refinement types were formalized in 1991 by Freeman and Pfenning as a means to integrate user-defined constraints into static checking. Subsequent developments expanded their scope, with the introduction of Liquid Types in 2008 by Rondon, Kawaguchi, and Jhala, which merged Hindley-Milner inference with predicate abstraction to verify complex invariants in functional languages like . Key concepts include subtyping rules that validate refinements through SMT-implied implications (e.g., ensuring a refined subtype satisfies 0 ≤ v < n), measures for quantifying data structure properties like list lengths, and path-sensitive analysis to handle branching logic. These features enable compositional verification, where function contracts propagate refinements automatically, supporting polymorphism and reflection for proof-carrying code. Refinement types have found applications in verifying safety properties, such as array bounds and memory safety in low-level languages like C, as well as functional correctness and termination in higher-level systems. Tools like Liquid Haskell (Vazou et al., 2014) embed refinements directly in Haskell code for theorem proving via SMT, while F* (Swamy et al., 2011) uses them for full-fledged program verification in a dependently typed setting. More recent advancements address challenges like heap reasoning and information flow security, making refinement types a cornerstone for practical formal verification in industry and academia.

Fundamentals

Definition

A refinement type augments a base type with a logical predicate that restricts the inhabitants of the type to those values satisfying the predicate, thereby enabling more precise specifications within a type system. This concept was originally developed as a refinement to ML's type system, allowing the declaration of recursively defined subtypes for user-defined datatypes while maintaining key properties of the underlying system. In formal notation, a refinement type is typically expressed as {v:T∣P(v)}\{v : T \mid P(v)\}, where TT is a base type such as integers and P(v)P(v) is a decidable predicate over values vv of type TT. For instance, the type of positive integers is denoted {v:\Int∣v>0}\{v : \Int \mid v > 0\}, which includes only integer values greater than zero. Refinement types extend naturally to function types, such as \Int→{n:\Int∣n>5}\Int \to \{n : \Int \mid n > 5\}, specifying that the output is an integer exceeding 5 regardless of the input. Refinement types serve as a lightweight form of dependent types, in which type-level predicates depend on runtime values to enforce invariants, and align with behavioral by using predicates to define contracts on program behavior. A distinguishing feature is their design to preserve decidable in languages like ML, ensuring that subtype checks and unification remain computable through restrictions on predicate expressiveness and finite subtype lattices. This balance allows for expressive value constraints without sacrificing the practicality of type checking.

Motivation

Traditional type systems, such as Hindley-Milner, offer coarse-grained guarantees like distinguishing integers from strings but cannot express fine-grained properties such as bounds on values (e.g., 1≤i≤991 \leq i \leq 99), non-nullness of pointers, or program invariants, often requiring expensive runtime checks to ensure safety. For instance, in languages like , base types fail to differentiate singleton lists from general lists, leading to potential runtime errors when code assumes non-emptiness, as the type checker cannot enforce such distinctions statically. Refinement types overcome these limitations by augmenting base types with logical predicates that precisely specify allowable values, enabling compile-time detection of errors, improved code safety through static verification, and the integration of formal specifications without unduly burdening programmers. This approach eliminates the need for runtime assertions in verified code paths, reducing overhead while maintaining expressiveness for critical properties like array bounds or resource limits. In comparison to dynamic typing, which postpones property checks until runtime and risks crashes or performance penalties from frequent validations, refinement types deliver static guarantees that enhance reliability from the outset. Relative to full dependent types, which provide arbitrary expressiveness but demand manual annotations and face undecidable challenges, refinement types achieve a practical balance by confining predicates to decidable logics (e.g., linear arithmetic), supporting automated and usability in real-world programming. A key application of refinement types lies in articulating preconditions and postconditions for functions, such as requiring positive inputs to avert or ensuring outputs adhere to invariants like sorted order, thereby preempting invalid arguments or results at . These predicate-based restrictions on base types allow developers to encode domain-specific constraints directly in signatures, fostering safer and more maintainable code.

Formalism

Syntax

Refinement types augment base types with logical predicates to specify subsets of values satisfying certain properties. The basic syntactic form is denoted as {v:τ∣ϕ}\{v : \tau \mid \phi\}, where τ\tau is a base type (such as Int\mathsf{Int} or Bool\mathsf{Bool}), vv is a fresh variable representing elements of the type, and ϕ\phi is a predicate that constrains the values. This notation allows precise descriptions, such as {x:Int∣x>0}\{x : \mathsf{Int} \mid x > 0\} for positive integers. Function types in refinement systems extend arrow types to include input and output refinements, capturing preconditions and postconditions. A refined function type is written as {x:τ1∣ϕ1}→{y:τ2∣ϕ2(x)}\{x : \tau_1 \mid \phi_1\} \to \{y : \tau_2 \mid \phi_2(x)\}, where ϕ1\phi_1 constrains the input xx and ϕ2\phi_2 (which may depend on xx) constrains the output yy. For instance, an increment function might have the {x:Int∣x>0}→{y:Int∣y=x+1}\{x : \mathsf{Int} \mid x > 0\} \to \{y : \mathsf{Int} \mid y = x + 1\}, ensuring the input is positive and the output is exactly one more than the input. Refinement types integrate with the Hindley-Milner system by treating refinements as additional constraints solved during unification. The inference process generates predicates from the program structure and uses SMT solvers to validate relations between refined types, ensuring decidability for supported logics while preserving polymorphism. The predicate language ϕ\phi is typically restricted to decidable fragments, such as quantifier-free linear integer arithmetic with equality and inequality, along with support for simple data types like booleans and tuples. Valid refinements include linear constraints like {n:Int∣0≤n∧n<10}\{n : \mathsf{Int} \mid 0 \leq n \land n < 10\} or equalities like {y:Int∣y=2⋅x}\{y : \mathsf{Int} \mid y = 2 \cdot x\} for even numbers derived from doubling. Invalid refinements in basic systems might involve nonlinear operations, such as quadratic inequalities, which exceed the supported decidable logic.

Semantics

In refinement type systems, the denotational semantics interprets a refined type {v:τ∣ϕ}\{v : \tau \mid \phi\} as the subset of the semantic domain of the base type τ\tau consisting of those values vv for which the refinement predicate ϕ\phi evaluates to true. More formally, the denotation [ ⁣[{x:τ∣r}] ⁣]={e∣∅⊢e:τ, if e↠∗w then r[w/x]↠∗⊤}[\![ \{x : \tau \mid r\} ]\! ] = \{ e \mid \emptyset \vdash e : \tau, \, \text{if } e \twoheadrightarrow^* w \text{ then } r[w/x] \twoheadrightarrow^* \top \}, where ee ranges over expressions that reduce to values ww satisfying the refinement rr. This set-theoretic view ensures that refinements partition the inhabitants of base types into logically constrained subsets, enabling precise specifications while preserving the underlying type structure. Type checking in refinement systems relies on subtyping rules grounded in predicate implication. For instance, {v:τ∣ϕ}\subtype{v:τ∣ψ}\{v : \tau \mid \phi\} \subtype \{v : \tau \mid \psi\} holds if ϕ  ⟹  ψ\phi \implies \psi, verified through logical entailment under the typing environment. Function subtyping follows a contravariant-covariant pattern: τ1→τ2\subtypeσ1→σ2\tau_1 \to \tau_2 \subtype \sigma_1 \to \sigma_2 if σ1\subtypeτ1\sigma_1 \subtype \tau_1 and τ2\subtypeσ2\tau_2 \subtype \sigma_2, extended to refinements via their denotations. Bidirectional type checking integrates these rules with satisfiability modulo theories (SMT) solvers to discharge verification conditions, such as environment assumptions implying refinement obligations, ensuring decidable and efficient validation. The soundness of refinement types is established through preservation and progress theorems, guaranteeing that well-typed programs under refinements neither diverge unexpectedly nor violate their predicates during reduction. Specifically, if ∅⊢Ue:τ\emptyset \vdash_U e : \tau and e↠e′e \twoheadrightarrow e', then ∅⊢Ue′:τ\emptyset \vdash_U e' : \tau (preservation), and if ∅⊢Ue:τ\emptyset \vdash_U e : \tau with ee not a value, then e↠e′e \twoheadrightarrow e' for some e′e' (progress). These properties extend to more expressive settings, such as those with effects or recursive data, by stratifying refinements to values in weak head normal form and restricting predicates to decidable fragments like quantifier-free equality and uninterpreted functions. Refinements are handled statically during type checking, where predicates are verified upfront to prevent runtime violations, though dynamic monitoring may occur in implementations. In gradual refinement type systems, which interleave refined and dynamic types, evaluation incorporates blame assignment to track errors arising from imprecise refinements, ensuring that type errors are attributed to the least refined component via cast insertion and locality principles.

Implementations

In functional programming languages

Refinement types have been notably integrated into functional programming languages through tools that extend their type systems with logical predicates, enabling precise verification of program properties at compile time. In Haskell, LiquidHaskell serves as a prominent implementation, operating as a plugin for the Glasgow Haskell Compiler (GHC) that embeds refinement type checking directly into the compilation process. It leverages annotations in the form of special comments to specify refinements, which are then verified using an SMT solver such as Z3 to discharge proof obligations automatically. This approach allows developers to refine standard types with predicates that enforce invariants, such as non-emptiness or bounded values, without altering the underlying Haskell code's executability. The syntax for refinements in LiquidHaskell uses pragmas like {-@ type Pos = {v:Int | v > 0} @-} to define a refined type Pos as positive integers, where {v:τ | e} denotes a base type τ refined by predicate e over value v. For instance, safe division can be verified by typing a function as {-@ safeDiv :: Int -> {v:Int | v != 0} -> Int @-}, ensuring the denominator is non-zero and preventing runtime errors through static checks. LiquidHaskell also supports refining data structures for properties like sortedness; a list type might be refined as {v:[Int] | sorted v} to guarantee ascending order, with the tool proving this invariant for functions operating on lists, such as merge operations. Similarly, for trees, refinements can enforce binary search tree invariants, verifying that all elements in the left subtree are less than the root and recursively so for subtrees. These capabilities have been applied to verify over 10,000 lines of real-world Haskell code, demonstrating practical utility in functional settings. Beyond , refinement types appear in other functional languages through specialized verifiers and extensions. In Scala, refinement types can be implemented via libraries such as refined, which constrain types with predicates checked at or runtime. Research on predicate-qualified types, a form of refinement types adapted to Scala's features, includes SMT-based prototypes embedded in early versions of the Dotty . As of 2025, new designs for logically qualified types in Scala 3, enabling static checking of logical predicates, are being prototyped. The Stainless verifier for Scala enables refinement-based proofs by annotating functions with preconditions and postconditions, using SMT solving to confirm properties like termination and absence of errors in a functional of the . For , early work on liquid types introduced refinement capabilities via the Dsolve tool, which infers dependent types from logical qualifiers to verify safety properties, such as array bounds, with minimal annotations in polymorphic higher-order functions. Despite these advances, implementing refinement types in pure functional languages faces challenges, particularly the scalability of SMT solving for complex predicates involving higher-order functions and . In contexts like , SMT-based checking can encounter unsoundness issues due to implicit assumptions about variable evaluation order, requiring careful handling of non-strict semantics to maintain verification reliability. Additionally, the computational cost of solving intricate constraints grows with program size, limiting applicability to large-scale functional codebases without optimizations like incremental solving.

In other languages and tools

In JavaScript and TypeScript, refinement types are supported through tools like Flow, which enable type narrowing based on conditional tests to refine unions into more precise subtypes. For instance, Flow allows refining a union type such as a string literal "A" or "B" into a singleton type after a conditional check, ensuring safer handling of dynamic values without full dependent types. This approach contrasts with TypeScript's built-in type guards, as Flow's refinements integrate predicate-based narrowing directly into the type system for better flow-sensitive analysis. Additionally, experimental extensions like Refined TypeScript (RSC) extend this to higher-order, imperative code by combining refinements with TypeScript's structural typing, facilitating static verification of properties like array bounds or null safety. In , refinement types are explored through specialized crates and frameworks that build on the language's model to enhance the borrow checker with predicate-based constraints. The tool, for example, introduces liquid-style refinements that verify properties like resource bounds or safety invariants at , integrating seamlessly with Rust's linear types to prevent runtime errors in systems code. achieves this by encoding refinements as traits with SMT-solvable predicates, allowing developers to annotate functions with constraints such as "this vector has length at least n" without altering core Rust syntax. More recently, as of 2025, introduces a prophecy-based refinement type system for Rust, using constrained solvers for automated inference and precise pointer reasoning. These efforts remain experimental, focusing on ergonomic verification for concurrent and low-level programming where traditional types fall short. Specialized tools extend refinement types to domain-specific languages, particularly in synchronous and embedded systems. Kind 2, a model checker for the Lustre language, incorporates SMT-based refinement types to restrict base types with logical predicates, enabling compositional verification of real-time properties in safety-critical applications like . In Lustre programs, refinements might specify that a variable remains true after a certain node activation, with Kind 2 using (SMT) solvers to prove adherence across hierarchical designs. For gradual typing scenarios, systems like those proposed in gradual refinement types research allow incremental adoption of refinements in dynamically typed languages, blending static predicates with runtime checks to support from untyped codebases. Refinement types are also encoded in proof assistants for cross-language verification, leveraging their foundations to formalize predicates over programs in various paradigms. In Coq, refinements can be embedded as proof-irrelevant predicates on base types, allowing verification of imperative or functional code by refining types with decidable constraints solved via tactics or external solvers. This encoding supports stepwise refinement calculus, where abstract specifications are gradually concretized while preserving correctness proofs. Similarly, Isabelle/HOL provides data refinement frameworks that refine abstract datatypes (e.g., sets) into efficient implementations, using locales and code generation to bridge formal proofs with executable code in languages like Scala or . These mechanisms enable modular proofs of refinement validity, ensuring that concrete operations simulate abstract ones under given invariants.

Applications

Program verification

Refinement types facilitate program verification by allowing developers to specify and enforce pre- and postconditions through refined function types, ensuring properties such as the absence of runtime errors like . For instance, a safe division function can be typed as divide :: x:Int -> {v:Int | v != 0} -> {v:Int | v * snd == fst}, where the refinement on the second argument guarantees a non-zero denominator, and the postcondition verifies the mathematical correctness of the result; the verifier automatically checks these constraints using logical implications derived from the program's . In practice, refinement types enable proofs of algorithmic properties, such as sortedness in sorting algorithms. For implemented in , the merge function can be refined to preserve ordering: merge :: (IsSorted xs, IsSorted ys) -> {v: [a] | IsSorted v /\ [Permutation](/page/Permutation) xs ys v}, where IsSorted is a refinement predicate ensuring non-decreasing order, and Permutation confirms the output contains the same elements; the verifier inductively proves this for the recursive split-and-merge steps, confirming the overall algorithm produces a sorted list. Similarly, totality of recursive functions is verified by refining measures that decrease with each call, such as list lengths in , ensuring termination without infinite loops. Refinement types integrate with automated theorem provers, particularly SMT solvers like Z3, to discharge verification conditions by translating refinement obligations into queries; this handles quantifier instantiation and equality reasoning, enabling scalable proofs without manual intervention for many programs. Advanced applications refine abstract data types to maintain structural invariants, such as balance in red-black trees, where node colors and heights are encoded in refinements like RBTree c h ensuring no two red nodes are adjacent and black-height balance; insertion and deletion operations are verified to restore these invariants post-rebalancing, preventing degradation to linear . Tools like LiquidHaskell exemplify this integration for programs.

Static analysis and error detection

Refinement types enable compile-time checks for common errors such as null dereferences, array bounds violations, and type mismatches by attaching logical predicates to base types, allowing static verifiers to prove that values satisfy these constraints before execution. For instance, a type like {v: int | v != null} ensures non-null values, preventing dereference errors, while {v: int | 0 <= v < len(a)} enforces array index bounds to avoid out-of-bounds access. Type mismatches are detected through subsorting rules that validate predicate compatibility, such as ensuring an refinement aligns with expected numeric operations. These checks are performed via bidirectional type checking, which infers and verifies refinements simultaneously, as implemented in systems like datasorts for functional languages. In tools like Flow, a static type checker for , refinements support conditional narrowing to refine types based on runtime-like tests at , enhancing error detection. For example, given a value of type string | null, a check if (value != null) narrows it to string within the branch, allowing safe operations and flagging potential null dereferences elsewhere with warnings like sketchy-null. Similarly, employs discriminated unions as a lightweight form of refinement, where a shared property narrows union types for precise ; for instance, a union of shapes with a kind field enables the type checker to infer Circle or Square in switch branches, catching accesses to incompatible properties like radius on a square. These mechanisms integrate refinements into environments, balancing expressiveness with usability. Studies on codebases show that tools incorporating refinement-like features, such as Flow and , detect approximately 15% of bugs at , including type mismatches and null/undefined accesses, thereby reducing reliance on runtime handling. With 's strict null checks, detection of null-related bugs increases by 58% compared to looser configurations, minimizing the need for explicit null validations in code. These gains establish the practical impact of refinements in scaling static analysis to large, dynamic codebases. Despite these benefits, refinement types face limitations, including false positives arising from contexts or incomplete predicate resolution, which can reject valid code unless manually adjusted. More fundamentally, predicates relying on SMT solvers for verification are undecidable in general, potentially leading to timeouts or inconclusive results for complex constraints, thus requiring user-provided annotations to guide —typically 1-3% of code lines in practice. These annotations ensure decidability within restricted logics but impose a verification overhead on developers.

History

Origins and early work

The origins of refinement types trace back to the early , when researchers sought to enhance the expressiveness of type systems in programming languages like ML without sacrificing decidable . In 1991, Tim Freeman and Frank Pfenning introduced the concept in their work on refining subsets of ML, where they augmented types with predicates to define subtypes of user-defined datatypes, such as distinguishing non-empty lists from general lists. This approach preserved ML's principal types and decidable inference by restricting refinements to finite lattices, allowing the system to detect more errors at while remaining compatible with existing ML programs. Their seminal paper, "Refinement Types for ML," emphasized practical error detection in polymorphic functions, exemplified by refining types to prevent operations like lastcons from being applied to empty lists, which would otherwise cause runtime failures in . The system combined techniques with an type discipline, enabling recursive subtype definitions (e.g., via rectype declarations) that refined algebraic datatypes without introducing undecidable checks. This foundational contribution balanced precision and usability, influencing subsequent designs. Refinement types drew roots from earlier ideas in dependent types, as seen in systems like NuPRL, which integrated computational and logical specifications into types, and from subtyping principles, including the that ensures subtypes behave compatibly with supertypes. These influences allowed refinement types to extend ML's Hindley-Milner system conservatively, adding expressive predicates while maintaining decidability—a core property that aligns with the semantic foundations of and dependency. Early extensions built on this foundation in the late , with Hongwei Xi and Frank Pfenning developing the Dependent ML (DML) system in 1999 to support richer refinements, particularly for eliminating array bound checks through index-dependent types. DML integrated expressions into type indices, enabling decidable verification of bounds and other properties in ML-like programs, thus expanding the scope of refinement types beyond basic datasort predicates to more general dependent constraints.

Recent developments

The 2010s marked a significant surge in the practical application of refinement types, transitioning from theoretical foundations to tools integrated into popular programming languages. LiquidHaskell, introduced by Vazou et al., extended Haskell's type system with refinement types verified via SMT solvers, enabling the specification and proof of properties like termination and safety for over 10,000 lines of real-world code with minimal annotations. Concurrently, Flow, developed by (now Meta), brought refinement types to in 2014, allowing developers to express precise constraints on dynamic values and improve error detection in large-scale web applications. In the 2020s, innovations have focused on enhancing and expressiveness. A notable advancement is refinement type refutations, proposed by Webbers et al. in 2024, which provide compositional explanations for type-checking failures by generating counterexamples that mirror the structure of the program, improving debugging in refinement-based verifiers. Research trends emphasize scalability and domain-specific extensions. Efforts in scalable SMT integration, as seen in ongoing LiquidHaskell developments, have optimized solver interactions to handle larger codebases efficiently. Refinements for concurrency, exemplified by for introduced in 2023, leverage ownership types to verify and invariants in parallel programs. Emerging work on AI-assisted predicate generation, such as the neurosymbolic LHC system by Sakkas et al. (2025), uses large language models to infer modular refinement annotations, reducing manual effort in verification. As of , refinement types enjoy widespread industry adoption, notably in Meta's Hack language, where built-in type refinements enforce precise constraints on classes and interfaces for safer PHP-derived code at scale. Ongoing explores higher-order refinements to support more expressive specifications, such as quantified predicates over functions, promising further integration with advanced type systems.

References

  1. https://arxiv.org/abs/2010.07763
  2. https://www.cs.cmu.edu/~fp/papers/pldi91.pdf
  3. https://dl.acm.org/doi/10.1145/1375581.1375602
  4. https://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf
  5. https://patrickrondon.com/research/papers/liquid-types-pldi08.pdf
  6. https://dl.acm.org/doi/pdf/10.1145/113446.113468
  7. https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/MSR-TR-2009-147-SP1.pdf
  8. https://goto.ucsd.edu/~nvazou/real_world_liquid.pdf
  9. https://www.cs.cmu.edu/~rwh/students/davies.pdf
  10. https://simon.peytonjones.org/assets/pdfs/refinement-types-for-haskell.pdf
  11. https://dl.acm.org/doi/10.1145/3009837.3009856
  12. https://ucsd-progsys.github.io/liquidhaskell-tutorial/
  13. https://github.com/fthomas/refined
  14. https://dl.acm.org/doi/10.1145/2998392.2998398
  15. https://2025.workshop.scala-lang.org/details/scala-2025/11/Logically-Qualified-Types-for-Scala-3
  16. https://epfl-lara.github.io/stainless/
  17. https://goto.ucsd.edu/~nvazou/haskell-refinements-techrep.pdf
  18. https://cs.pomona.edu/~michael/papers/iclp2020_sub.pdf
  19. https://flow.org/en/docs/lang/refinements/
  20. https://dl.acm.org/doi/10.1145/2908080.2908110
  21. https://ranjitjhala.github.io/static/refinement_types_for_typescript.pdf
  22. https://dl.acm.org/doi/10.1145/3591283
  23. https://github.com/flux-rs/flux
  24. https://dl.acm.org/doi/10.1145/3729333
  25. https://www.youtube.com/watch?v=NIJtZ0yUDX0
  26. https://kind.cs.uiowa.edu/kind2_user_docs/v2.2.0/2_input/4_refinement_types.html
  27. https://dl.acm.org/doi/10.1145/3674657
  28. https://www.cs.cmu.edu/~fp/papers/tlca09.pdf
  29. https://www.sciencedirect.com/science/article/pii/S0167642317300710
  30. https://www21.in.tum.de/~haftmann/pdf/data_refinement_in_isabelle_hol_haftmann_krauss_kuncar_nipkow.pdf
  31. https://www.complang.tuwien.ac.at/kps2015/proceedings/KPS_2015_submission_13.pdf
  32. https://ucsd-progsys.github.io/liquidhaskell-tutorial/book.pdf
  33. https://arxiv.org/pdf/1701.03320
  34. http://goto.ucsd.edu/~gridaphobe/liquid/haskell/blog/blog/2013/07/29/putting-things-in-order.lhs
  35. https://dl.acm.org/doi/10.1145/3158141
  36. https://www.typescriptlang.org/docs/handbook/2/narrowing.html
  37. https://goto.ucsd.edu/~pvekris/docs/pldi16.pdf
  38. https://www.microsoft.com/en-us/research/wp-content/uploads/2017/09/gao2017javascript.pdf
  39. https://dl.acm.org/doi/10.1145/113445.113468
  40. https://dl.acm.org/doi/10.1145/292540.292560
  41. https://www.cs.cmu.edu/~fp/papers/pldi98dml.pdf
  42. https://dl.acm.org/doi/10.1145/2633357.2633366
  43. https://engineering.fb.com/2014/11/18/web/flow-a-new-static-type-checker-for-javascript/
  44. https://dl.acm.org/doi/10.1145/3689745
  45. https://arxiv.org/abs/2207.05617
  46. https://dl.acm.org/doi/10.1109/ICSE55347.2025.00090
  47. https://docs.hhvm.com/hack/types/with-refinement
  48. https://arxiv.org/abs/2509.15005
Add your contribution
Related Hubs
Contribute something
User Avatar
No comments yet.