Relating Church-Style and Curry-Style Subtyping

Adriana Compagnoni, Healfdene Goguen

Type theories with higher-order subtyping or singleton types are examples of systems where computation rules for variables are affected by type information in the context. A compli…