Research and Reading

Polarized Subtyping

Publications

• Polarized Subtyping

In-Queue / In-Use

Classics

• Call-by-push-value_ A subsuming paradigm
• Types are not sets
• Tree automata techniques and applications

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

Type-level (meta) Operations and Concatenation

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

Step Indexing

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