Extensible Datasort Refinements
Abstract
Refinement types turn typechecking into lightweight verification. The classic form of refinement type is the datasort refinement, in which datasorts identify subclasses of inductive datatypes.
Related papers
- A Higher-Order Logic for Concurrent Termination-Preserving Refinement ESOP 2017
- Verifying replicated data types with typeclass refinements in Liquid Haskell OOPSLA 2020
- Feature featherweight java: a calculus for feature-oriented programming and stepwise refinement GPCE 2008
- Deterministic parallelism via liquid effects PLDI 2012
- An effective theory of type refinements ICFP 2003
- PLEX: Normalization for Refinement Types OOPSLA 2026
- Formalizing, Mechanizing, and Verifying Class-Based Refinement Types ECOOP 2024
- Pushouts in software architecture design GPCE 2012