More specifically, Coq is based on the calculus of inductive constructions: https://en.m.wikipedia.org/wiki/Calculus_of_constructions https://en.m.wikipedia.org

More specifically, Coq is based on the calculus of inductive constructions: https://en.m.wikipedia.org/wiki/Calculus_of_constructions https://en.m.wikipedia.org/wiki/Calculus_of_constructions. The key differentiating feature being dependent types, whereas Isabelle/HOL implements higher-order logic without dependent types.