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)

• Inheritance is subtyping

Theory

• Sequent calculi for induction and infinite descent

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

Type-level (meta) Operations and Concatenation

• A calculus with recursive types, record concatenation and subtyping
• Operations on records

Semantic Typing & Step Indexing

• Step-indexed syntactic logical relations for recursive and quantified types
• Semantics of types for mutable state