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

(29)

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

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)