Refinement Types for Incremental Computational Complexity ( Technical Appendix )

– four new types: type variable X, universal type ∀X : K.τ , type operator abstraction λi :: S.τ and type operator application τ I. – A new kinding judgment Ψ; ∆ ` T :: K that assigns kinds to types – Typing judgment ∆; Φ; Γ ` e :κ τ changes to Ψ; ∆; Φ; Γ ` e :κ τ in which the context Ψ binds the type variables. – The subtyping judgment is changed as follows: Ψ; ∆; Φ |= τ1 v τ2 : K. – Semantics of kinds, annotated J−KK – Semantics of types is indexed by a type substitution environment ρ which must lie in the interpretation T JΨK. We also add corresponding type interpretations for newly added types.