constructive mathematics, realizability, computability propositions as types, proofs as programs, computational trinitarianism A thunk-force category is a category that models call-by-value programming languages with effects. More commonly, terms in a call-by-value language are modelled as morphisms in the Kleisli category of a strong monad. A thunk-force category axiomatizes the Kleisli category directly and is also called an abstract Kleisli category1. The original category can be recovered...