An effective theory of type refinements

DOI10.1145/944705.944725zbMATH Open1315.68055OpenAlexW2032687731MaRDI QIDQ5261277FDOQ5261277

Authors:

Publication date: 2 July 2015

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

Full work available at URL: https://doi.org/10.1145/944705.944725

Recommendations

• Refinement types for program analysis
• A relational model of types-and-effects in higher-order concurrent separation logic
• A bidirectional refinement type system for LF
• Bounded refinement types
• The type and effect discipline

zbMATH Keywords

linear logictype theorylocal reasoningeffectful computationtype refinement

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Cited In (13)

• ν-Types for Effects and Freshness Analysis
• Title not available (Why is that?)
• Refining inductive types
• Principles and applications of refinement types
• Title not available (Why is that?)
• Roles, stacks, histories: a triple for Hoare
• Types and trace effects for object orientation
• Roles, stacks, histories: A triple for Hoare
• Static typing for a substructural lambda calculus
• Shallow embedding of type theory is morally correct
• Title not available (Why is that?)
• Programming Languages and Systems
• Hoare type theory, polymorphism and separation

This page was built for publication: An effective theory of type refinements

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