Refinement types for Haskell

By Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, Simon L. Peyton Jones. ACM SIGPLAN International Conference on Functional Programming, 2014

300 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Dependent types and multi-monadic effects in F* (2016, background): “More recently, old-F ⋆ (Swamy et al. 2013a) adds value-dependent types to an ML-like language; Rondon et al. (2008) add decidable, reﬁnement types to OCaml and Vazou et al. (2014) adapt that work to Haskell—we have compared these prior reﬁnement type systems to F ⋆ in § 3.2.”
OptTyper: Probabilistic Type Inference by Optimising Logical and Natural Constraints (2020, background): “LiquidHaskell [Vazou et al. 2014] is a static verifier of Haskell based on Liquid Types via SMT and predicate abstraction.”
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy (2014, unknown): “Figure 2: Relational interpretation of assertions”
Refinement types for TypeScript (2016, background): “The extensibility and modularity offered by refinement types have enabled their use in a variety of applications in typed, functional languages, like ML [28, 40], Haskell [37], and F ] [33].”