An effective theory of type refinements

DOI10.1145/944705.944725MaRDI QIDQ5261277zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

effectful computationlinear logiclocal reasoningtype refinementtype theory

Mathematics Subject Classification ID

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

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

Cited in

(20)

• Types and trace effects for object orientation
• Shallow embedding of type theory is morally correct
• A theory of gradual effect systems
• A bidirectional refinement type system for LF
• Refining inductive types
• Bounded refinement types
• Roles, stacks, histories: a triple for Hoare
• Principles and applications of refinement types
• Roles, stacks, histories: A triple for Hoare
• ν-Types for Effects and Freshness Analysis
• Static typing for a substructural lambda calculus
• Hoare type theory, polymorphism and separation
• scientific article; zbMATH DE number 1265030 (Why is no real title available?)
• An Isbell duality theorem for type refinement systems
• scientific article; zbMATH DE number 785045 (Why is no real title available?)
• scientific article; zbMATH DE number 1420793 (Why is no real title available?)
• A relational model of types-and-effects in higher-order concurrent separation logic
• Programming Languages and Systems
• Logic of refinement types
• Exception tracking in an open world

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)