Bounded refinement types

DOI10.1145/2784731.2784745MaRDI QIDQ2981942zbMATH OpenOpenAlexFDO

Authors Niki Vazou, Alexander Bakst, Ranjit Jhala

Publication date 10 May 2017

Published in Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1507.00385

zbMATH Keywords

abstract interpretationrefinement typesHaskell

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Database theory (68P15) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Abstract: We present a notion of bounded quantification for refinement types and show how it expands the expressiveness of refinement typing by using it to develop typed combinators for: (1) relational algebra and safe database access, (2) Floyd-Hoare logic within a state transformer monad equipped with combinators for branching and looping, and (3) using the above to implement a refined IO monad that tracks capabilities and resource usage. This leap in expressiveness comes via a translation to "ghost" functions, which lets us retain the automated and decidable SMT based checking and inference that makes refinement typing effective in practice.

Recommendations

• Abstract refinement types
• Principles and applications of refinement types
• Refinement types for Haskell
• An effective theory of type refinements
• Gradual refinement types

Cited in

(4)

• Abstract refinement types
• Principles and applications of refinement types
• An effective theory of type refinements
• Embedded domain specific verifiers

Describes a project that uses

Uses Software

• Haskell

This page was built for publication: Bounded refinement types

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