Simple type system for call-by-value calculus with first-class continuations and environments

In this paper, we propose a simple type system for the call-by-value lambda calculus with first-class continuations and environments. We give typing rules of the simple type system and show subject reduction theorem of the type system, which means that a typing of a term is preserved during reduction.