Research and Reading
Polarized Subtyping
In-Queue
Classics
- Call-by-push-value_ A subsuming paradigm
- Types are not sets
- Tree automata techniques and applications
- Type systems
Subtyping (General)
Theory
Intersection Types
- Monadic intersection types, relationally
- Intersection types and computational effects
- A tale of intersection types
- Programming with union, intersection, and negation types
- The duality of classical intersection and union types
- Intersection and union types_ Syntax and semantics
- Hybrid intersection types for PCF (extended version)
Refinement Types
- Contextual refinement types
- Refinement kinds_ type-safe programming with practical type-level computation
- Type refinements in an open world (extended abstract)
- Structural refinement types
- Practical refinement-type checking
- Refinement types and computational duality
- Refinement types for haskell