Here are two that are implemented in non-functional languages:

• Arend is implemented in Java.
• Lean 3 is implemented in C++.

Note that Lean 3 has since been supplemented by Lean 4, which is implemented (mostly) in Lean 4.

Which programming language is used to implement a proof assistant is orthogonal to the language used by the proof assistant, although of course it might be harder to implement a proof assistant with Excel macros than in an ML-style language.

Here are three that are implemented in non-functional languages:

• Arend is implemented in Java.
• Lean 3 is implemented in C++.
• Metamath has verifiers implemented in C, Rust, Javascript, Mathematica, Python, etc.

(Note that Lean 4, while still having some C++ core functionality, is moving heavily towards being implemented in Lean 4.)

Which programming language is used to implement a proof assistant is orthogonal to the language used by the proof assistant, although of course it might be harder to implement a proof assistant with Excel macros than in an ML-style language.