Operational characterization of solvability in a bi-typed λ-calculus with mixed evaluation order
Introduction to a polarized abstract-machine-like calculi, and explanation of its relationship with call-by-push-value
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