A general semantic construction of dependent refinement type systems, categorically

DOI10.1007/978-3-030-71995-1_21OpenAlexW3141317606MaRDI QIDQ2233424

Satoshi Kura

Publication date: 18 October 2021

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

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Notions of computation and monads
• Categorical logic and type theory
• Weakest preconditions in fibrations
• Dependent Types and Fibred Computational Effects
• Towards a Formal Theory of Graded Monads
• Refinement types for Haskell
• Functors are Type Refinement Systems
• Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy
• Abstract Refinement Types
• Hybrid type checking
• Gradual refinement types
• Secure distributed programming with value-dependent types
• Parametric effect monads and semantics of effect systems

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