Operational characterization of solvability in a bi-typed λ-calculus with mixed evaluation order
Operationally characterization of solvability in a polarized abstract-machine-like calculus
Weak reduction for open term in call-by-push-value via a polarised intuitionnistic abstract-machine-like calculi