<p>Obviously there is an <a href="http://www.ii.uni.wroc.pl/~mabi/papers/PPDP13.pdf" rel="noreferrer">operational semantics of Ltac</a> by Jedynak et al.</p>

CC BY-SA 4.0
2018-10-24T02:09:22.600Z
2018-10-24T02:09:22.600Z
xrq
<p>I'm not sure this answers your question, but the first (?) paper on the subject of tactics appears to have been Milner's <em><a href="http://rsta.royalsocietypublishing.org/content/312/1522/411" rel="noreferrer">The Use of Machines to Assist in Rigorous Proof</a></em>.</p>

CC BY-SA 4.0
2018-10-24T06:49:12.503Z
2018-10-24T06:49:12.503Z
Martin Berger
<p>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. </p>

<p>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?</p>

<pl.programming-languages><semantics><proof-assistants>
Formal semantics of tactics
xrq
# Formal semantics of tactics

(Asked by: username_0 on 2018-10-24)

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?

**Tags:** pl.programming-languages, semantics, proof-assistants


---

## 2 answers

### Answer by username_1 on 2018-10-24. Score: 8 | Accepted answer

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](http://rsta.royalsocietypublishing.org/content/312/1522/411)*.


---

### Answer by username_0 on 2018-10-24. Score: 8

Obviously there is an [operational semantics of Ltac](http://www.ii.uni.wroc.pl/~mabi/papers/PPDP13.pdf) by Jedynak et al.


---

