Refinement types for Haskell

DOI10.1145/2628136.2628161MaRDI QIDQ2819690zbMATH OpenOpenAlexFDO

Authors Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, Simon Peyton-Jones

Publication date 29 September 2016

Published in Proceedings of the 19th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.495.9202

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Gradual refinement types
• Static contract checking for Haskell
• Abstract refinement types
• Refinement types for program analysis
• Sums of uncertainty: refinements go gradual

Cited in

(30)

• Proving type class laws for Haskell
• Learning inductive invariants by sampling from frequency distributions
• A general semantic construction of dependent refinement type systems, categorically
• Temporal refinements for guarded recursive types
• Type Class Instances for Type-Level Lambdas in Haskell
• Semantic subtyping with an SMT solver
• Bounded refinement types
• Modular verification of higher-order functional programs
• Refinement types for Ruby
• Parametricity for Haskell with Imprecise Error Semantics
• LiquidHaskell
• Ready, set, verify! Applying hs-to-coq to real-world Haskell code
• ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
• Semantic subtyping for non-strict languages
• Liquid types for array invariant synthesis
• Semantic subtyping with an SMT solver
• Static contract checking for Haskell
• Abstract refinement types
• Gradual refinement types
• Sums of uncertainty: refinements go gradual
• Higher order symbolic execution for contract verification and refutation
• Fissile type analysis, modular checking of almost everywhere invariants
• Parameterized recursive refinement types for automated program verification
• Embedded domain specific verifiers
• On algebraic array theories
• Manifest contracts with intersection types
• Succinct ordering and aggregation constraints in algebraic array theories
• Dependent type refinements for futures
• Reasoning about incompletely defined programs
• MiniSail - A kernel language for the ISA specification language SAIL

Describes a project that uses

Uses Software

• Haskell

This page was built for publication: Refinement types for Haskell

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2819690)