Formal semantics of tactics

Tactics are supposed to represent inference rules in a system, and it might seem unnecessary at first to formalize the semantics of tactics; nevertheless, modern theorem provers can have pretty complicated tactics which have complex semantics.

My question is, thus, has there been any work on the formalization of tactics in interactive theorem proving, either for Coq-style or LCF/HOL-style theorem provers?

Asked by user46269 (1,125 )
Oct 24, 2018 at 00:36