Is there a calculus of explicit substitution that is confluent on open terms, simulates one-step beta-reduction and preserves beta-strong normalization?

The source page states the original problem together with its recorded qualifications and progress updates as follows.

There are confluent calculi of explicit substitutions but these do not preserve termination (strong normalization) [Kesner, 1998], and there are calculi that are not confluent on open terms but which do preserve termination [Kesner, 1998]. C'esar Mu~noz presented in~[Kesner, 1998] a calculus enjoying both properties (answering RTALooP entry explicit-substitution), however, the calculus is not able to simulate one-step of beta-reduction: if $a$ beta-reduces to $b$ in the lambda-calculus then $a$ does not necessarily reduce to $b$ in the calculus of Mu~{n}oz. Is there a calculus of explicit substitution that is confluent on open terms, simulates one-step beta-reduction and preserves beta-strong normalization?

Recorded update.

Submitted by Jean Goubault-Larrecq on Mon Nov 27 16:37:43 MET 2000.

This problem was solved positively in [Kesner, 1998]. The calculus SKInT, introduced in [Kesner, 1998], is confluent on open terms and simulates one-step beta-reduction (although in a slightly contorted way, see [Kesner, 1998]; the obvious translation only simulates a bit more that one-step call-by-value beta-reduction). The paper [Kesner, 1998] characterizes strongly normalizing, weakly normalizing and solvable terms through intersection types, and preservation of strong normalization follows. SKInT is also standardizing, has a terminating subcalculus of substitutions $\Sigma T$, but is based on an infinite signature and finitely many rule schemes parameterized by integers. Can we lift the latter restriction?