A general semantic construction of dependent refinement type systems, categorically

DOI10.1007/978-3-030-71995-1_21MaRDI QIDQ2233424zbMATH OpenOpenAlexFDO

Authors Satoshi Kura

Publication date 18 October 2021

Copyright license Creative Commons Attribution 4.0 International

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

Mathematics Subject Classification ID

Theory of software (68Nxx) Theory of computing (68Qxx)

Cites work

• scientific article; zbMATH DE number 2163037 (Why is no real title available?)
• Abstract refinement types
• Categorical logic and type theory
• Dependent types and fibred computational effects
• Functors are type refinement systems
• Gradual refinement types
• Higher-order approximate relational refinement types for mechanism design and differential privacy
• Hybrid type checking
• Notions of computation and monads
• Parametric effect monads and semantics of effect systems
• Refinement types for Haskell
• Secure distributed programming with value-dependent types
• Towards a formal theory of graded monads
• Weakest preconditions in fibrations

Cited in

(2)

• Extensional and Intensional Semantic Universes
• scientific article; zbMATH DE number 4099299 (Why is no real title available?)

This page was built for publication: A general semantic construction of dependent refinement type systems, categorically

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