6
$\begingroup$

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?

|cite|improve this question
$\endgroup$
8
$\begingroup$

I'm not sure this answers your question, but the first (?) paper on the subject of tactics appears to have been Milner's The Use of Machines to Assist in Rigorous Proof.

|cite|improve this answer
$\endgroup$
8
$\begingroup$

Obviously there is an operational semantics of Ltac by Jedynak et al.

|cite|improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.